diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-20 22:05:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-20 22:05:06 +0000 |
| commit | 0bddb9049651406c4ce5549626c77c4c382a0288 (patch) | |
| tree | 4da8322bf547cc7c2624bdfc2d9ca24a346218cb /pretyping | |
| parent | 5e4bca70bd87a20364ec5867476bbef4912aefdc (diff) | |
Bug prédicat old Case/Match
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1176 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1b0928c10..70d826790 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -373,18 +373,19 @@ let rec pretype tycon env isevars lvar lmeta = function let dep = find_case_dep_nparams env !isevars (cj.uj_val,pj.uj_val) indf evalPt in - let (p,pt) = (* Buggé ... mettre le lambda après les realargs *) + let (p,pt) = if dep then (pj.uj_val, evalPt) else 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 + | IsLambda (_,_,c) -> decomp (n-1) c | _ -> 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 ind = build_dependent_inductive indf in + let s' = mkProd (Anonymous, ind, s) in let ccl = lift 1 (decomp n pj.uj_val) in - let ccl' = mkLambda (Anonymous, mkAppliedInd indt, ccl) in + let ccl' = mkLambda (Anonymous, ind, 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 |