Change the option for cumulativity

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