diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-07-07 14:09:31 +0200 |
|---|---|---|
| committer | Amin Timany <amintimany@gmail.com> | 2017-07-31 18:05:54 +0200 |
| commit | fbe0b2645eab84012aec50e76d94e15a3fefe664 (patch) | |
| tree | 40aa5ddc6c55f889b1d92b547b5d48d02bd5e23c | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
Issue error on monomorphic cumulative inductives
| -rw-r--r-- | test-suite/success/cumulativity.v | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index ebf817cfc..604da2108 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -1,3 +1,9 @@ +Polymorphic Cumulative Inductive T1 := t1 : T1. +Fail Monomorphic Cumulative Inductive T2 := t2 : T2. + +Polymorphic Cumulative Record R1 := { r1 : T1 }. +Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}. + Set Universe Polymorphism. Set Inductive Cumulativity. Set Printing Universes. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6b04ff00a..3542c4081 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 |