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 6131f4c03..6f2b3c4b2 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -516,7 +516,7 @@ let is_sort_variable uctx s =
| _ -> None
let subst_univs_context_with_def def usubst (ctx, cst) =
- (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+ (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst)
let normalize_variables uctx =
let normalized_variables, undef, def, subst =