From 3159dac77f2d822f2fe40c2b3b4a941da4e0265c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 21 Sep 2007 17:57:13 +0000
Subject: curpat_ty was in a smaller context

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

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index c1889b689c..e54c59058f 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1743,7 +1743,7 @@ let build_ineqs prevpatterns pats liftsign =
 			  len',
 			  succ n, (* nth pattern *)
 			  mkApp (Lazy.force eq_ind,
-				[| lift (len + liftsign) ppat_ty ;
+				[| lift (succ len') curpat_ty ;
 				   liftn (len + liftsign) (succ lens) ppat_c ;
 				   lift len' curpat_c |]) :: 
 			    List.map (lift lens (* Jump over this prevpat signature *)) c)
-- 
cgit v1.2.3