diff options
| author | Gaëtan Gilbert | 2018-11-06 22:49:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:08:46 +0100 |
| commit | 55cb4f64ccd95f639e6ae375e8de3014f73d2bcb (patch) | |
| tree | 3e0dd203a4a888b606c42e45652c9e03a6c4f3b5 /kernel/vars.ml | |
| parent | 563623f4eeb9d9992b1bffb5b71a6b849ba71132 (diff) | |
Fix lifting in foo_with_full_binders for (co)fixpoints
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 17 |
1 files changed, 3 insertions, 14 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 7380a860dd..f9c576ca4a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Esubst module RelDecl = Context.Rel.Declaration @@ -80,19 +79,9 @@ let noccur_with_meta n m term = (* Lifting *) (*********************) -(* The generic lifting function *) -let rec exliftn el c = match Constr.kind c with - | Constr.Rel i -> Constr.mkRel(reloc_rel i el) - | _ -> Constr.map_with_binders el_lift exliftn el c - -(* Lifting the binding depth across k bindings *) - -let liftn n k c = - match el_liftn (pred k) (el_shft n el_id) with - | ELID -> c - | el -> exliftn el c - -let lift n = liftn n 1 +let exliftn = Constr.exliftn +let liftn = Constr.liftn +let lift = Constr.lift (*********************) (* Substituting *) |