Bugs calcul du prédicat des Cases et Case

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1119 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 3 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 55574d235..c6fe2cbcb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1038,7 +1038,7 @@ let build_initial_predicate env sigma isdep pred tomatchl =
 	Some (List.map (lift n) realargs), Some (lift n c)
     | c,NotInd _ -> None, Some (lift n c) in
   let decomp_lam_force p =
-    match kind_of_term (whd_betadeltaiota env sigma p) with
+    match kind_of_term p with
       | IsLambda (_,_,c) -> c
       | _ -> (* eta-expansion *) applist (lift 1 pred, [mkRel 1]) in
   let rec strip_and_adjust nargs pred =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e7292c387..1b0928c10 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -375,8 +375,17 @@ let rec pretype tycon env isevars lvar lmeta = function
 
       let (p,pt) = (* Buggé ... mettre le lambda après les realargs *)
 	if dep then (pj.uj_val, evalPt) else
-	  (mkLambda (Anonymous, mkAppliedInd indt, lift 1 pj.uj_val),
-	   mkProd (Anonymous, mkAppliedInd indt, lift 1 evalPt)) in
+	  let n = List.length realargs in
+	  let rec decomp n p =
+	    if n=0 then p else
+	      match kind_of_term p with
+		| IsLambda (_,_,c) -> decomp (n-1) p
+		| _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) in
+	  let sign,s = decompose_prod_n n evalPt in
+	  let s' = mkProd (Anonymous, mkAppliedInd indt, lift 1 evalPt) in
+	  let ccl = lift 1 (decomp n pj.uj_val) in
+	  let ccl' = mkLambda (Anonymous, mkAppliedInd indt, ccl) in
+	  (lam_it ccl' sign, prod_it s' sign) in
       let (bty,rsty) =
 	Indrec.type_rec_branches isrec env !isevars indt pt p cj.uj_val in
       if Array.length bty <> Array.length lf then