aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 5c7a529b9c..9dc106a3d7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -660,7 +660,8 @@ val fix_undefined_variables : evar_map -> evar_map
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
-val update_sigma_env : evar_map -> env -> evar_map
+(** Lift [UState.update_sigma_univs] *)
+val update_sigma_univs : UGraph.t -> evar_map -> evar_map
(** Polymorphic universes *)