aboutsummaryrefslogtreecommitdiff
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, 0 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 679173ca72..3f17e63034 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
val fix_undefined_variables : evar_map -> evar_map
-val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
-
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map