diff options
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 6 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | test-suite/coqchk/cumulativity.v | 2 | ||||
| -rw-r--r-- | test-suite/success/cumulativity.v | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
6 files changed, 13 insertions, 13 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 0bce22f58..027ba16f0 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -167,9 +167,9 @@ let use_polymorphic_flag () = let make_polymorphic_flag b = local_polymorphic_flag := Some b -let inductive_cumulativity = ref false -let make_inductive_cumulativity b = inductive_cumulativity := b -let is_inductive_cumulativity () = !inductive_cumulativity +let polymorphic_inductive_cumulativity = ref false +let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b +let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity (** [program_mode] tells that Program mode has been activated, either globally via [Set Program] or locally via the Program command prefix. *) diff --git a/lib/flags.mli b/lib/flags.mli index eb4c37a54..5af563b46 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,9 +119,9 @@ val is_universe_polymorphism : unit -> bool val make_polymorphic_flag : bool -> unit val use_polymorphic_flag : unit -> bool -(** Global inductive cumulativity flag. *) -val make_inductive_cumulativity : bool -> unit -val is_inductive_cumulativity : unit -> bool +(** Global polymorphic inductive cumulativity flag. *) +val make_polymorphic_inductive_cumulativity : bool -> unit +val is_polymorphic_inductive_cumulativity : unit -> bool val warn : bool ref val make_warn : bool -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3d29fca77..568818c27 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -169,7 +169,7 @@ GEXTEND Gram let cum = match cum with Some b -> b - | None -> Flags.is_inductive_cumulativity () + | None -> Flags.is_polymorphic_inductive_cumulativity () in VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index a978f6b90..7906a5b15 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 8854435cf..0ee85712e 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -5,7 +5,7 @@ Polymorphic Cumulative Record R1 := { r1 : T1 }. Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}. Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3542c4081..12a31953c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1369,10 +1369,10 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "inductive cumulativity"; - optkey = ["Inductive"; "Cumulativity"]; - optread = Flags.is_inductive_cumulativity; - optwrite = Flags.make_inductive_cumulativity } + optname = "Polymorphic inductive cumulativity"; + optkey = ["Polymorphic"; "Inductive"; "Cumulativity"]; + optread = Flags.is_polymorphic_inductive_cumulativity; + optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = declare_int_option |