From fbe0b2645eab84012aec50e76d94e15a3fefe664 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 14:09:31 +0200
Subject: Issue error on monomorphic cumulative inductives

---
 vernac/vernacentries.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6b04ff00a0..3542c4081e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,7 +522,12 @@ 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 vernac_record cum k poly finite struc binders sort nameopt cfs =
+  check_cumulativity_polymorphism_flag cum poly;
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -540,6 +545,7 @@ 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 cum poly lo finite indl =
+  check_cumulativity_polymorphism_flag cum poly;
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
-- 
cgit v1.2.3


From 3b7e7f7738737475cb0f09130b0487c85906dd2b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 13:29:36 +0200
Subject: Change the option for cumulativity

---
 vernac/vernacentries.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3542c4081e..12a31953c5 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
-- 
cgit v1.2.3


From e333c2fa6d97e79b389992412846adc71eb7abda Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 17:41:38 +0200
Subject: 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.
---
 vernac/vernacentries.ml | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 12a31953c5..1556beb060 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
-- 
cgit v1.2.3