Merge PR #9439: Separate variance and universe fields in inductives.

Ack-by: ppedrot

1 files changed, 4 insertions, 5 deletions

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