diff options
| -rw-r--r-- | vernac/vernacentries.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bb8df512ca..dec5a79892 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -762,16 +762,6 @@ let vernac_inductive ~atts cum lo kind indl = ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") -(* - - match indl with - | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> - let f = - let (coe, ({loc;v=id}, ce)) = l in - let coe' = if coe then Some true else None in - (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] - *) let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then |