1 files changed, 17 insertions, 11 deletions

diff --git a/engine/uState.mli b/engine/uState.mli
index 48c38faf..f833508e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,7 +26,7 @@ val empty : t
 
 val make : UGraph.t -> t
 
-val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -34,9 +34,9 @@ val union : t -> t -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
-val of_binders : Universes.universe_binders -> t
+val of_binders : UnivNames.universe_binders -> t
 
-val universe_binders : t -> Universes.universe_binders
+val universe_binders : t -> UnivNames.universe_binders
 
 (** {5 Projections} *)
 
@@ -44,7 +44,7 @@ val context_set : t -> Univ.ContextSet.t
 (** The local context of the state, i.e. a set of bound variables together
     with their associated constraints. *)
 
-val subst : t -> Universes.universe_opt_subst
+val subst : t -> UnivSubst.universe_opt_subst
 (** The local universes that are unification variables *)
 
 val ugraph : t -> UGraph.t
@@ -79,7 +79,7 @@ val add_constraints : t -> Univ.Constraint.t -> t
   @raise UniversesDiffer when universes differ
 *)
 
-val add_universe_constraints : t -> Universes.Constraints.t -> t
+val add_universe_constraints : t -> UnivProblem.Set.t -> t
 (**
   @raise UniversesDiffer when universes differ
 *)
@@ -103,8 +103,8 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
-val merge_subst : t -> Universes.universe_opt_subst -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
@@ -137,11 +137,17 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 (** Universe minimization *)
 val minimize : t -> t
-val normalize : t -> t
-[@@ocaml.deprecated "Alias of UState.minimize"]
+
+type ('a, 'b) gen_universe_decl = {
+  univdecl_instance : 'a; (* Declared universes *)
+  univdecl_extensible_instance : bool; (* Can new universes be added *)
+  univdecl_constraints : 'b; (* Declared constraints *)
+  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
 
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (lident list, Univ.Constraint.t) gen_universe_decl
+
+val default_univ_decl : universe_decl
 
 (** [check_univ_decl ctx decl]
 
@@ -165,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t