Infrastructure for cumulative inductive syntax (no grammar extension yet)

4 files changed, 15 insertions, 2 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index bb26ce652e..6b37958ab3 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,6 +367,12 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
+let variance_of_entry ~cumulative = function
+  | Monomorphic_entry _ -> None
+  | Polymorphic_entry (nas,_) ->
+    Some (Array.map (fun _ -> None) nas)
+(* TODO syntax to have non-None elements *)
+
 let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
@@ -429,7 +435,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
       mind_entry_template = is_template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = variance_of_entry ~cumulative uctx;
     }
   in
   mind_ent, Evd.universe_binders sigma
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 91e8f609d5..1d9de11fcc 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -86,3 +86,6 @@ val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:
 (** [nparams] is the number of parameters which aren't treated as
     uniform, ie the length of params (including letins) where the env
     is [uniform params, inductives, params, binders]. *)
+
+val variance_of_entry : cumulative:bool -> Entries.universes_entry
+  -> Univ.Variance.t option array option
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index bef9e29ac2..c4f7e77714 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -744,6 +744,9 @@ let explain_bad_relevance env =
 let explain_bad_invert env =
   strbrk "Bad case inversion (maybe a bugged tactic)."
 
+let explain_bad_variance env sigma u =
+  str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma u ++ str"."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -788,6 +791,7 @@ let explain_type_error env sigma err =
   | DisallowedSProp -> explain_disallowed_sprop ()
   | BadRelevance -> explain_bad_relevance env
   | BadInvert -> explain_bad_invert env
+  | BadVariance u -> explain_bad_variance env sigma u
 
 let pr_position (cl,pos) =
   let clpos = match cl with
diff --git a/vernac/record.ml b/vernac/record.ml
index 891d7fcebe..e2e9bbd967 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -568,7 +568,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat
       mind_entry_private = None;
       mind_entry_universes = univs;
       mind_entry_template = template;
-      mind_entry_cumulative = poly && cumulative;
+      mind_entry_variance = ComInductive.variance_of_entry ~cumulative univs;
     }
   in
   let impls = List.map (fun _ -> paramimpls, []) record_data in