aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 202f6232da..fd65d7de50 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -2003,7 +2003,6 @@ let subst_univs_constraints subst csts =
(fun c cstrs -> subst_univs_constraint subst c cstrs)
csts Constraint.empty
-
let subst_instance_level s l =
match l.Level.data with
| Level.Var n -> s.(n)