From 8fb5eeef9efe3873b10c4f14ba06a1883bc38aac Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 18 Oct 2011 09:33:57 +0000
Subject: Fix inductive coercion code in Program (bug #2378)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14571 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_coercion.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 5a2d840570..74f31a901f 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -141,7 +141,7 @@ module Coercion = struct
 		let restargs = lift_args 1
 		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
 		in
-		let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
+		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
 		let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in
 		let evar = make_existential loc env isevars eq in
-- 
cgit v1.2.3