diff options
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 13 |
2 files changed, 12 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 55574d235f..c6fe2cbcbf 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 e7292c387c..1b0928c102 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 |