aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vars.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vars.ml')
-rw-r--r--kernel/vars.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 40a797a90..120c07d30 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -299,5 +299,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)