diff options
| author | Amin Timany | 2017-07-07 14:09:31 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-07-31 18:05:54 +0200 |
| commit | fbe0b2645eab84012aec50e76d94e15a3fefe664 (patch) | |
| tree | 40aa5ddc6c55f889b1d92b547b5d48d02bd5e23c /vernac | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
Issue error on monomorphic cumulative inductives
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6b04ff00a0..3542c4081e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -522,7 +522,12 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom +let check_cumulativity_polymorphism_flag cum poly = + if cum && not poly then + user_err Pp.(str "Monomorphic cumulative inductive types/records are not supported. ") + let vernac_record cum k poly finite struc binders sort nameopt cfs = + check_cumulativity_polymorphism_flag cum poly; let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -540,6 +545,7 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive cum poly lo finite indl = + check_cumulativity_polymorphism_flag cum poly; if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with |