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 4f2ece900..d166fd804 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -556,6 +556,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