aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 555c3a150c..b20700143f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1160,8 +1160,8 @@ let universe_binders evd = UState.universe_binders evd.universes
let universes evd = UState.ugraph evd.universes
-let update_sigma_env evd env =
- { evd with universes = UState.update_sigma_env evd.universes env }
+let update_sigma_univs ugraph evd =
+ { evd with universes = UState.update_sigma_univs evd.universes ugraph }
exception UniversesDiffer = UState.UniversesDiffer