From b677b4ef232b8919d9b3bda4917111125def0de7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 11 Jul 2004 21:07:05 +0000
Subject: Eta-expansion du predicat dans build_indrec (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5887 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b0f68b67be..3645c49155 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -297,12 +297,12 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 		  if dep then (Anonymous,None,depind)::lnames' else lnames' in
 		it_mkLambda_or_LetIn_name env
 		  (appvect
-		    (mkRel ((if dep then nar+1 else nar) + dect + j),
+		    (mkRel ((if dep then 1 else 0) + dect + j),
 		    extended_rel_vect 0 arsign)) arsign
 	      in
 	      it_mkLambda_or_LetIn_name env
 		(lambda_create env
-		  (depind,mkCase (ci, lift 1 p, mkRel 1, branches)))
+		  (depind,mkCase (ci, lift (nar+1) p, mkRel 1, branches)))
 		lnames'
 	    in
 	    let typtyi = 
-- 
cgit v1.2.3