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

---
 engine/eConstr.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index cfc4bea85f..40e48998d6 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -296,6 +296,8 @@ let decompose_prod_n_assum sigma n c =
 
 let existential_type = Evd.existential_type
 
+let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
+
 let map_under_context f n c =
   let f c = unsafe_to_constr (f (of_constr c)) in
   of_constr (Constr.map_under_context f n (unsafe_to_constr c))
@@ -453,11 +455,11 @@ let iter_with_full_binders sigma g f n c =
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i t)) n) n lna tl in
     Array.iter (f n') bl
   | CoFix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in
     Array.iter (f n') bl
 
 let iter_with_binders sigma g f n c =
@@ -712,7 +714,7 @@ let to_rel_decl = unsafe_to_rel_decl
 type substl = t list
 
 (** Operations that commute with evar-normalization *)
-let lift n c = of_constr (Vars.lift n (to_constr c))
+let lift = lift
 let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
 
 let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c))
-- 
cgit v1.2.3