aboutsummaryrefslogtreecommitdiff
path: root/kernel/vars.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vars.ml')
-rw-r--r--kernel/vars.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a9f4644abf..40a797a902 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,7 +295,7 @@ let subst_univs_level_constr subst c =
if u' == u then t else
(changed := true; mkSort (Sorts.sort_of_univ u'))
| _ -> Constr.map aux t
- in
+ in
let c' = aux c in
if !changed then c' else c