aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 9e975da58..c271d9d99 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -306,7 +306,7 @@ let pr_evar_universe_context ctx =
str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
str"UNDEFINED UNIVERSES:"++brk(0,1)++
- h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
+ h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
str "WEAK CONSTRAINTS:"++brk(0,1)++
h 0 (UState.pr_weak prl ctx) ++ fnl ())