Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

5 files changed, 25 insertions, 41 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8493119ee5..8756ebfdf2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    cstrs
-  | Declarations.Polymorphic_ind _ ->
-     enforce_eq_instances_univs false u1 u2 cstrs
-  | Declarations.Cumulative_ind cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> enforce_eq_instances_univs false u1 u2 cstrs
+  | Some variances ->
     let num_param_arity = Reduction.inductive_cumulativity_arguments spec in
-    let variances = Univ.ACumulativityInfo.variance cumi in
     compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    cstrs
-  | Declarations.Polymorphic_ind _ ->
-    enforce_eq_instances_univs false u1 u2 cstrs
-  | Declarations.Cumulative_ind cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> enforce_eq_instances_univs false u1 u2 cstrs
+  | Some _ ->
     let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
diff --git a/engine/evd.ml b/engine/evd.ml
index eee2cb700c..f0433d3387 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes
 
 let to_universe_context evd = UState.context evd.universes
 
-let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
-let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
+
+let const_univ_entry = univ_entry
 
 let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
diff --git a/engine/evd.mli b/engine/evd.mli
index de73144895..d2d18ca486 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -597,12 +597,12 @@ val universes : evar_map -> UGraph.t
     [Univ.ContextSet.to_context]. *)
 val to_universe_context : evar_map -> Univ.UContext.t
 
-val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
 
-(** NB: [ind_univ_entry] cannot create cumulative entries. *)
-val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
+val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
 
-val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 430a3a2fd9..77d1896683 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -100,24 +100,16 @@ let constraints ctx = snd ctx.uctx_local
 
 let context ctx = ContextSet.to_context ctx.uctx_local
 
-let const_univ_entry ~poly uctx =
+let univ_entry ~poly uctx =
   let open Entries in
   if poly then
     let (binders, _) = uctx.uctx_names in
     let uctx = context uctx in
     let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
-    Polymorphic_const_entry (nas, uctx)
-  else Monomorphic_const_entry (context_set uctx)
+    Polymorphic_entry (nas, uctx)
+  else Monomorphic_entry (context_set uctx)
 
-(* does not support cumulativity since you need more info *)
-let ind_univ_entry ~poly uctx =
-  let open Entries in
-  if poly then
-    let (binders, _) = uctx.uctx_names in
-    let uctx = context uctx in
-    let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
-    Polymorphic_ind_entry (nas, uctx)
-  else Monomorphic_ind_entry (context_set uctx)
+let const_univ_entry = univ_entry
 
 let of_context_set ctx = { empty with uctx_local = ctx }
 
@@ -422,10 +414,10 @@ let check_univ_decl ~poly uctx decl =
       let (binders, _) = uctx.uctx_names in
       let uctx = universe_context ~names ~extensible uctx in
       let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
-      Entries.Polymorphic_const_entry (nas, uctx)
+      Entries.Polymorphic_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
-      Entries.Monomorphic_const_entry uctx.uctx_local
+      Entries.Monomorphic_entry uctx.uctx_local
   in
   if not decl.univdecl_extensible_constraints then
     check_implication uctx
@@ -458,8 +450,8 @@ let restrict ctx vars =
 let demote_seff_univs entry uctx =
   let open Entries in
   match entry.const_entry_universes with
-  | Polymorphic_const_entry _ -> uctx
-  | Monomorphic_const_entry (univs, _) ->
+  | Polymorphic_entry _ -> uctx
+  | Monomorphic_entry (univs, _) ->
     let seff = LSet.union uctx.uctx_seff_univs univs in
     { uctx with uctx_seff_univs = seff }
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 5170184ef4..a358813825 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -64,12 +64,11 @@ val constraints : t -> Univ.Constraint.t
 val context : t -> Univ.UContext.t
 (** Shorthand for {!context_set} with {!Context_set.to_context}. *)
 
-val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
-val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
-(** Pick from {!context} or {!context_set} based on [poly].
-    Cannot create cumulative entries. *)
+val const_univ_entry : poly:bool -> t -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
 
 (** {5 Constraints handling} *)
 
@@ -177,7 +176,7 @@ val default_univ_decl : universe_decl
    When polymorphic, the universes corresponding to
    [decl.univdecl_instance] come first in the order defined by that
    list. *)
-val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry
 
 val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t