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, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 76fa69e31..8c3771cd9 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context
val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
evar_universe_context
val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
-val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context
val evar_universe_context_of_binders :