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/eConstr.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 743888a9be..b0e834b2e7 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,11 +201,11 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
-val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
+val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
 
 (** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *)
-val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
 
 val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
-- 
cgit v1.2.3