diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-25 18:47:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-25 18:47:13 +0000 |
| commit | 5e9e77da344315c1d85e72d0d53941580717b067 (patch) | |
| tree | 111c97911a5aea8fc74d8533b836429208e6f58a /pretyping | |
| parent | c96e8baeb12706668ad1544f46b45088cc65ca2a (diff) | |
Bug prédicat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1199 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ca61af805..19a3950b7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -587,8 +587,7 @@ let abstract_conclusion typ cs = let (sign,p) = decompose_prod_n n typ in lam_it p sign -let infer_predicate env isevars typs cstrs (IndType (indf,_) as indt) = - let IndFamily (mis,_) = indf in +let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) = (* Il faudra substituer les isevars a un certain moment *) if Array.length cstrs = 0 then (* "TODO4-3" *) error "Inference of annotation for empty inductive types not implemented" @@ -600,7 +599,7 @@ let infer_predicate env isevars typs cstrs (IndType (indf,_) as indt) = if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns then (* Non dependent case -> turn it into a (dummy) dependent one *) - let sign = (Anonymous,None,mkAppliedInd indt)::sign in + let sign = (Anonymous,None,build_dependent_inductive indf)::sign in let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in (true,pred) (* true = dependent -- par défaut *) else @@ -730,12 +729,11 @@ let specialize_predicate_match tomatchs cs = function (* Ne perd-on pas des cas en ne posant pas true à la place de dep ? *) (fun ((na,t),_) p -> PrProd ((dep,na,t),p)) tomatchs pred'' -let find_predicate env isevars p typs cstrs current - (IndType (indf,realargs) as indt) = +let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) = let (dep,pred) = match p with | Some p -> abstract_predicate env !isevars indf p - | None -> infer_predicate env isevars typs cstrs indt in + | None -> infer_predicate env isevars typs cstrs indf in let typ = whd_beta (applist (pred, realargs)) in if dep then (pred, whd_beta (applist (typ, [current])), Type Univ.dummy_univ) |