Improve errors for cumulativity when monomorphic

We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.

6 files changed, 46 insertions, 14 deletions

diff --git a/API/API.mli b/API/API.mli
index 19726b52f..d39d3cb25 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3780,6 +3780,12 @@ sig
     | DefaultInline
     | InlineAt of int
 
+  type cumulative_inductive_parsing_flag =
+    | GlobalCumulativity
+    | GlobalNonCumulativity
+    | LocalCumulativity
+    | LocalNonCumulativity
+
   type vernac_expr =
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_expr Loc.located
@@ -3804,7 +3810,7 @@ sig
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
       inline * (plident list * Constrexpr.constr_expr) with_coercion list
-  | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 6ef9532ad..2adf522b7 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -305,6 +305,14 @@ 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
+
 (** {6 The type of vernacular expressions} *)
 
 type vernac_expr =
@@ -336,7 +344,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * (plident list * constr_expr) with_coercion list
-  | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 568818c27..93a778274 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -168,8 +168,13 @@ GEXTEND Gram
           let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
 	  let cum =
 	    match cum with
-	      Some b -> b
-	    | None -> Flags.is_polymorphic_inductive_cumulativity ()
+	      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" ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 379c83b24..e3010e3b5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1471,7 +1471,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1486,7 +1486,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a68b569cb..4c50c2f36 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -760,7 +760,11 @@ open Decl_kinds
                        | Class _ -> "Class" | Variant -> "Variant"
           in
           if p then
-            let cm = if cum then "Cumulative" else "NonCumulative" in
+            let cm =
+              match cum with
+              | GlobalCumulativity | LocalCumulativity -> "Cumulative"
+              | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+            in
             cm ^ " " ^ kind
           else kind
         in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 12a31953c..1556beb06 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,12 +522,21 @@ 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 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.")
 
 let vernac_record cum k poly finite struc binders sort nameopt cfs =
-  check_cumulativity_polymorphism_flag cum poly;
+  let is_cumulative = should_treat_as_cumulative cum poly in
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -538,14 +547,14 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort))
 
 (** When [poly] is true the type is declared polymorphic. When [lo] is true,
     then the type is declared private (as per the [Private] keyword). [finite]
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive cum poly lo finite indl =
-  check_cumulativity_polymorphism_flag cum poly;
+  let is_cumulative = should_treat_as_cumulative cum poly in
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -582,7 +591,7 @@ let vernac_inductive cum poly lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl cum poly lo finite
+    do_mutual_inductive indl is_cumulative poly lo finite
 
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in