Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

4 files changed, 30 insertions, 43 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index ea6ed8321d..175f9c66df 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -143,7 +143,7 @@ let declare_constant_common id cst =
   update_tables c;
   c
 
-let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
+let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
@@ -156,8 +156,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let is_poly de = match de.const_entry_universes with
-  | Monomorphic_const_entry _ -> false
-  | Polymorphic_const_entry _ -> true
+  | Monomorphic_entry _ -> false
+  | Polymorphic_entry _ -> true
   in
   let in_section = Lib.sections_are_opened () in
   let export, decl = (* We deal with side effects *)
@@ -217,8 +217,8 @@ let cache_variable ((sp,_),o) =
          section-local definition, but it's not enforced by typing *)
       let (body, uctx), () = Future.force de.const_entry_body in
       let poly, univs = match de.const_entry_universes with
-      | Monomorphic_const_entry uctx -> false, uctx
-      | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+      | Monomorphic_entry uctx -> false, uctx
+      | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union uctx univs in
       (* We must declare the universe constraints before type-checking the
@@ -328,21 +328,15 @@ let dummy_inductive_entry m = {
   mind_entry_record = None;
   mind_entry_finite = Declarations.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
-  mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
+  mind_entry_universes = default_univ_entry;
+  mind_entry_variance = None;
   mind_entry_private = None;
 }
 
 (* reinfer subtyping constraints for inductive after section is dischared. *)
-let infer_inductive_subtyping mind_ent =
-  match mind_ent.mind_entry_universes with
-  | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
-    mind_ent
-  | Cumulative_ind_entry (_, cumi) ->
-    begin
-      let env = Global.env () in
-      (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-        InferCumulativity.infer_inductive env mind_ent
-    end
+let rebuild_inductive mind_ent =
+  let env = Global.env () in
+  InferCumulativity.infer_inductive env mind_ent
 
 let inInductive : mutual_inductive_entry -> obj =
   declare_object {(default_object "INDUCTIVE") with
@@ -352,25 +346,19 @@ let inInductive : mutual_inductive_entry -> obj =
     classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
     discharge_function = discharge_inductive;
-    rebuild_function = infer_inductive_subtyping }
+    rebuild_function = rebuild_inductive }
 
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
-  let univs = match univs with
-    | Monomorphic_ind_entry _ ->
+  let univs, u = match univs with
+    | Monomorphic_entry _ ->
       (* Global constraints already defined through the inductive *)
-      Monomorphic_const_entry Univ.ContextSet.empty
-    | Polymorphic_ind_entry (nas, ctx) ->
-      Polymorphic_const_entry (nas, ctx)
-    | Cumulative_ind_entry (nas, ctx) ->
-      Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
-  in
-  let term, types = match univs with
-    | Monomorphic_const_entry _ -> term, types
-    | Polymorphic_const_entry (_, ctx) ->
-      let u = Univ.UContext.instance ctx in
-      Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+      default_univ_entry, Univ.Instance.empty
+    | Polymorphic_entry (nas, ctx) ->
+      Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
   in
+  let term = Vars.subst_instance_constr u term in
+  let types = Vars.subst_instance_constr u types in
   let entry = definition_entry ~types ~univs term in
   let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
diff --git a/interp/declare.mli b/interp/declare.mli
index 669657af6f..6f53d6872b 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -43,7 +43,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?univs:Entries.constant_universes_entry ->
+  ?univs:Entries.universes_entry ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -58,7 +58,7 @@ val declare_constant :
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> Id.t -> ?types:constr ->
-  constr Entries.in_constant_universes_entry -> Constant.t
+  constr Entries.in_universes_entry -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
diff --git a/interp/discharge.ml b/interp/discharge.ml
index eeda5a6867..353b0f6057 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -76,18 +76,16 @@ let process_inductive info modlist mib =
   let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
   let subst, ind_univs =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
-    | Polymorphic_ind auctx ->
+    | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
+    | Polymorphic auctx ->
       let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
       let nas = Univ.AUContext.names auctx in
       let auctx = Univ.AUContext.repr auctx in
-      subst, Polymorphic_ind_entry (nas, auctx)
-    | Cumulative_ind cumi ->
-      let auctx = Univ.ACumulativityInfo.univ_context cumi in
-      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
-      let nas = Univ.AUContext.names auctx in
-      let auctx = Univ.AUContext.repr auctx in
-      subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
+      subst, Polymorphic_entry (nas, auctx)
+  in
+  let variance = match mib.mind_variance with
+    | None -> None
+    | Some _ -> Some (InferCumulativity.dummy_variance ind_univs)
   in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
@@ -114,6 +112,7 @@ let process_inductive info modlist mib =
     mind_entry_params = params';
     mind_entry_inds = inds';
     mind_entry_private = mib.mind_private;
+    mind_entry_variance = variance;
     mind_entry_universes = ind_univs
   }
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 60056dfd90..2f516f4f3c 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,12 +107,12 @@ let transl_with_decl env base kind = function
     let c, ectx = interp_constr env sigma c in
     let poly = lookup_polymorphism env base kind fqid in
     begin match UState.check_univ_decl ~poly ectx udecl with
-      | Entries.Polymorphic_const_entry (nas, ctx) ->
+      | Entries.Polymorphic_entry (nas, ctx) ->
         let inst, ctx = Univ.abstract_universes nas ctx in
         let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
         let c = EConstr.to_constr sigma c in
         WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
-      | Entries.Monomorphic_const_entry ctx ->
+      | Entries.Monomorphic_entry ctx ->
         let c = EConstr.to_constr sigma c in
         WithDef (fqid,(c, None)), ctx
     end