From 97d8ace6d013cd18eacd11357a13cd51dde3ab4e Mon Sep 17 00:00:00 2001
From: clrenard
Date: Tue, 12 Jun 2001 16:21:39 +0000
Subject: 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
---
 pretyping/cases.ml | 4 ++--
 1 file 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 =
-- 
cgit v1.2.3