aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/term.ml')
-rw-r--r--checker/term.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/term.ml b/checker/term.ml
index ad26c5edc..0f8aa804f 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -478,5 +478,5 @@ let subst_univs_level_constr subst c =
let c' = aux c in
if !changed then c' else c
-let subst_univs_context s =
- map_rel_context (subst_univs_constr s)
+let subst_univs_level_context s =
+ map_rel_context (subst_univs_level_constr s)