Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

3 files changed, 12 insertions, 16 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index d2d1efcb2c..4329b2d743 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -28,11 +28,8 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     | PrimRecord data -> Some (Some (Array.map pi1 data))
   in
   let mind_entry_universes = match mb.mind_universes with
-    | Monomorphic_ind univs -> Monomorphic_ind_entry univs
-    | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx)
-    | Cumulative_ind auctx ->
-      Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx),
-                            ACumulativityInfo.repr auctx)
+    | Monomorphic univs -> Monomorphic_entry univs
+    | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
   in
   let mind_entry_inds = Array.map_to_list (fun ind ->
       let mind_entry_arity, mind_entry_template = match ind.mind_arity with
@@ -64,6 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_params = mb.mind_params_ctxt;
     mind_entry_inds;
     mind_entry_universes;
+    mind_entry_variance = mb.mind_variance;
     mind_entry_private = mb.mind_private;
   }
 
@@ -135,7 +133,8 @@ let check_same_record r1 r2 = match r1, r2 with
 let check_inductive env mind mb =
   let entry = to_entry mb in
   let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
-        mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes;
+        mind_nparams; mind_nparams_rec; mind_params_ctxt;
+        mind_universes; mind_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set the oracle for further typechecking *)
@@ -157,6 +156,7 @@ let check_inductive env mind mb =
 
   check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt);
   ignore mind_universes; (* Indtypes did the necessary checking *)
+  ignore mind_variance; (* Indtypes did the necessary checking *)
   ignore mind_private; (* passed through Indtypes *)
 
   ignore mind_typing_flags;
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index c33c6d5d09..b86d491d72 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -16,8 +16,8 @@ let check_constant_declaration env kn cb =
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
-    | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
-    | Polymorphic_const auctx ->
+    | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+    | Polymorphic auctx ->
       let ctx = Univ.AUContext.repr auctx in
       let env = push_context ~strict:false ctx env in
       true, env
diff --git a/checker/values.ml b/checker/values.ml
index 7ca2dc8050..66467fa8f5 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -112,7 +112,6 @@ let v_variance = v_enum "variance" 3
 
 let v_instance = Annot ("instance", Array v_level)
 let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
-let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
@@ -226,14 +225,14 @@ let v_cst_def =
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
-let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
+let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
     v_constr;
     Any;
-    v_const_univs;
+    v_univs;
     Opt v_context_set;
     v_bool;
     v_typing_flags|]
@@ -276,10 +275,6 @@ let v_record_info =
   v_sum "record_info" 2
     [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
 
-let v_ind_pack_univs = 
-  v_sum "abstract_inductive_universes" 0
-    [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
-
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
     v_record_info;
@@ -289,7 +284,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_ind_pack_univs; (* universes *)
+    v_univs; (* universes *)
+    Opt (Array v_variance);
     Opt v_bool;
     v_typing_flags|]