aboutsummaryrefslogtreecommitdiffhomepage
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 cb22a2e2f..f23d5fc2c 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -104,7 +104,7 @@ let lift n = liftn n 1
type info = Closed | Open | Unknown
type 'a substituend = { mutable sinfo: info; sit: 'a }
-let rec lift_substituend depth s =
+let lift_substituend depth s =
match s.sinfo with
| Closed -> s.sit
| Open -> lift depth s.sit