From e242bab34b0b74bc1a02eaf750056d2684d72c36 Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Tue, 4 Apr 2017 13:43:11 +0200
Subject: end of correction of bug 4306

---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index d6a67219ff..a380443fe3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -291,7 +291,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
       *)
       let sub = Int.Map.bindings sub in
-      List.fold_left (fun end_of_type (i,t)  -> lift 1 (substnl  [t] (i-1) end_of_type))
+      List.fold_left (fun end_of_type (i,t)  -> liftn 1 i (substnl  [t] (i-1) end_of_type))
 	end_of_type_with_pop
 	sub
     in
-- 
cgit v1.2.3