From 55cb4f64ccd95f639e6ae375e8de3014f73d2bcb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Nov 2018 22:49:11 +0100
Subject: Fix lifting in foo_with_full_binders for (co)fixpoints

---
 kernel/vars.ml | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

(limited to 'kernel/vars.ml')

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    *)
-- 
cgit v1.2.3