Make parsing independent of the cumulativity flag.

5 files changed, 16 insertions, 32 deletions

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index df061bfb7..df746f765 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -297,13 +297,9 @@ type inline =
 type module_ast_inl = module_ast * inline
 type module_binder = bool option * lident list * module_ast_inl
 
-(** Cumulativity can be set globally, locally or unset locally and it
-   can not enabled at all. *)
-type cumulative_inductive_parsing_flag =
-  | GlobalCumulativity
-  | GlobalNonCumulativity
-  | LocalCumulativity
-  | LocalNonCumulativity
+(** [Some b] if locally enabled/disabled according to [b], [None] if
+    we should use the global flag. *)
+type cumulative_inductive_parsing_flag = bool option
 
 (** {6 The type of vernacular expressions} *)
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 72c3cc14a..7e7a887d3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -165,16 +165,6 @@ GEXTEND Gram
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
           let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-	  let cum =
-	    match cum with
-	      Some true -> LocalCumulativity
-            | Some false -> LocalNonCumulativity
-	    | None ->
-                if Flags.is_polymorphic_inductive_cumulativity () then
-                  GlobalCumulativity
-                else
-                  GlobalNonCumulativity
-	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (NoDischarge, recs)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 49f7aae43..319b410df 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1512,7 +1512,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1527,7 +1527,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5c5b7206a..b7f5a8309 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -788,8 +788,9 @@ open Decl_kinds
           if p then
             let cm =
               match cum with
-              | GlobalCumulativity | LocalCumulativity -> "Cumulative"
-              | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+              | Some true -> "Cumulative"
+              | Some false -> "NonCumulative"
+              | None -> ""
             in
             cm ^ " " ^ kind
           else kind
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3dbe8b0c0..479f9725e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl =
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let should_treat_as_cumulative cum poly =
-  if poly then
-    match cum with
-    | GlobalCumulativity | LocalCumulativity -> true
-    | GlobalNonCumulativity | LocalNonCumulativity -> false
-  else
-    match cum with
-    | GlobalCumulativity | GlobalNonCumulativity -> false
-    | LocalCumulativity -> 
-      user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
-    | LocalNonCumulativity ->
-      user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+  match cum with
+  | Some true ->
+    if poly then true
+    else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+  | Some false ->
+    if poly then false
+    else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+  | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
 
 let vernac_record cum k poly finite struc binders sort nameopt cfs =
   let is_cumulative = should_treat_as_cumulative cum poly in