Skip to content

Instantly share code, notes, and snippets.

@tomprince

tomprince/gist:1380905

Created November 20, 2011 21:02
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save tomprince/1380905 to your computer and use it in GitHub Desktop.
Save tomprince/1380905 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b0b0415..97e7794 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -415,7 +415,7 @@ let vernac_inductive finite infer indl =
| [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
let f =
let (coe, ((loc, id), ce)) = l in
- let coe' = if coe then Some false else None in
+ let coe' = if coe then Some true else None in
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
in vernac_record (Class true) finite infer id bl c None [f]
| [ ( id , bl , c , Class true, _), _ ] ->
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment