From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 17:58:08 +0200
Subject: Split off Universes functions dealing with names.

This API is a bit strange, I expect it will change at some point.
---
 engine/evd.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 509db525d9..7ce525744c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -550,7 +550,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 
 
 val evar_universe_context_of_binders :
-  Universes.universe_binders -> UState.t
+  UnivNames.universe_binders -> UState.t
 [@@ocaml.deprecated "Alias of UState.of_binders"]
 
 val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
@@ -559,7 +559,7 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
-val universe_binders : evar_map -> Universes.universe_binders
+val universe_binders : evar_map -> UnivNames.universe_binders
 val add_constraints_context : UState.t ->
   Univ.Constraint.t -> UState.t
 [@@ocaml.deprecated "Alias of UState.add_constraints"]
-- 
cgit v1.2.3


From 302adae094bbf76d8c951c557c85acb12a97aedc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 21:27:15 +0200
Subject: Split off Universes functions about substitutions and constraints

---
 engine/evd.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 7ce525744c..b2670ee518 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -354,7 +354,7 @@ val whd_sort_variable : evar_map -> econstr -> econstr
 
 exception UniversesDiffer
 
-val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map
+val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
 (** Add the given universe unification constraints to the evar map.
     @raise UniversesDiffer in case a first-order unification fails.
     @raise UniverseInconsistency .
@@ -543,7 +543,7 @@ val empty_evar_universe_context : UState.t
 val union_evar_universe_context : UState.t -> UState.t ->
   UState.t
 [@@ocaml.deprecated "Alias of UState.union"]
-val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst
+val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst
 [@@ocaml.deprecated "Alias of UState.subst"]
 val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 [@@ocaml.deprecated "Alias of UState.constrain_variables"]
@@ -603,7 +603,7 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 
 val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
-val universe_subst : evar_map -> Universes.universe_opt_subst
+val universe_subst : evar_map -> UnivSubst.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
 (** [to_universe_context evm] extracts the local universes and
@@ -622,7 +622,7 @@ val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
 
 val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
-val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
+val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
 
 val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
-- 
cgit v1.2.3