diff options
| author | msozeau | 2011-11-24 10:54:39 +0000 |
|---|---|---|
| committer | msozeau | 2011-11-24 10:54:39 +0000 |
| commit | 4484d5fc42c90bff13a1b9454a93b99b3fb94576 (patch) | |
| tree | 3ec42ef413f655843697d3ba147ecb24b67ee408 | |
| parent | 7b2bf4785916803c24629239aa746706fe3f6ef6 (diff) | |
Correct direction for definitional typeclasses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14722 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 916a305c22..8e370bc734 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, _), _ ] -> |