diff options
| author | clrenard | 2001-06-12 16:21:39 +0000 |
|---|---|---|
| committer | clrenard | 2001-06-12 16:21:39 +0000 |
| commit | 97d8ace6d013cd18eacd11357a13cd51dde3ab4e (patch) | |
| tree | 86ec34c7fc1401ea49daf87ac6c67cdb6227f188 | |
| parent | 2c58ecd5370c6b375b4933082d39bf76519d94f1 (diff) | |
Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes automatiquement.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1784 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index f69ca60846..3c0c3f05c1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -805,7 +805,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) = let predpred = it_mkLambda_or_LetIn (mkSort s) sign in let caseinfo = make_default_case_info mis in let brs = array_map2 abstract_conclusion typs cstrs in - let predbody = mkMutCase (caseinfo, predpred, mkRel 1, brs) in + let predbody = mkMutCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in (* "TODO4-2" *) error ("Unable to infer a Cases predicate\n"^ @@ -1131,7 +1131,7 @@ and match_current pb (n,tm) = pb.pred brtyps cstrs current indt in let ci = make_case_info mis None tags in pattern_status tags, - { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)pred,current,brvals); + { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)(nf_betaiota pred),current,brvals); uj_type = typ } and compile_further pb firstnext rest = |