aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index c40e925d8..405fcc403 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -552,6 +552,8 @@ val set_eq_instances : ?flex:bool ->
val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
+val check_constraints : evar_map -> Univ.Constraint.t -> bool
+
val evar_universe_context : evar_map -> UState.t
val universe_context_set : evar_map -> Univ.ContextSet.t
val universe_subst : evar_map -> UnivSubst.universe_opt_subst