Merge PR #7016: Make parsing independent of the cumulativity flag.

5 files changed, 21 insertions, 36 deletions

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 76b35b08f..06f969f19 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 vernac_cumulative = VernacCumulative | VernacNonCumulative
 
 (** {6 The type of vernacular expressions} *)
 
@@ -338,7 +334,7 @@ type nonrec vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
       inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8b445985b..593dcbf58 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -161,20 +161,10 @@ GEXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b)
       (* Gallina inductive declarations *)
-      | cum = cumulativity_token; priv = private_token; f = finite_token;
+      | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
         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)
@@ -257,7 +247,8 @@ GEXTEND Gram
       | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
   cumulativity_token:
-    [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ]
+    [ [ IDENT "Cumulative" -> VernacCumulative
+      | IDENT "NonCumulative" -> VernacNonCumulative ] ]
   ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
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 bbf0e2b60..7eb8396ac 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -767,8 +767,9 @@ open Decl_kinds
           if p then
             let cm =
               match cum with
-              | GlobalCumulativity | LocalCumulativity -> "Cumulative"
-              | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+              | Some VernacCumulative -> "Cumulative"
+              | Some VernacNonCumulative -> "NonCumulative"
+              | None -> ""
             in
             cm ^ " " ^ kind
           else kind
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0e8ca2289..b44c7cccb 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 VernacCumulative ->
+    if poly then true
+    else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+  | Some VernacNonCumulative ->
+    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
@@ -565,7 +562,6 @@ 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 ~atts cum lo finite indl =
-  let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -602,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
+    let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
     ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
 
 let vernac_fixpoint ~atts discharge l =