aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 6c8dbe3f4..df50bae86 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs =
let univs = ctx.uctx_universes in
let vars = ref ctx.uctx_univ_variables in
let weak = ref ctx.uctx_weak_constraints in
- let normalize = normalize_univ_variable_opt_subst vars in
+ let normalize u = normalize_univ_variable_opt_subst !vars u in
let nf_constraint = function
| ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
| UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)