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 81ab3dd66..0791e4c27 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -583,7 +583,7 @@ let refresh_constraints univs (ctx, cstrs) =
in ((ctx, cstrs'), univs')
let normalize_variables uctx =
- let normalized_variables, undef, def, subst =
+ let normalized_variables, def, subst =
UnivSubst.normalize_univ_variables uctx.uctx_univ_variables
in
let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in