diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 07454337f..cd30eaf5c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -415,7 +415,8 @@ let vernac_inductive finite infer indl = | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in - (((coe, AssumExpr ((loc, Name id), ce)), None), []) + let coe' = if coe then Some false 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, _), _ ] -> Util.error "Definitional classes must have a single method" |