From ad85c27c453e888e4ef44f3531645638faff3da2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Dec 2002 10:36:21 +0000
Subject: Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la
 possibilité de partage)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3416 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 31dd7e08a0..7b72de6092 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -290,7 +290,7 @@ let judge_of_case env ci pj cj lfj =
   let (_,kind) = dest_arity env pj.uj_type in
   let lft = Array.map j_type lfj in
   let univ' = check_branch_types env cj (lft,bty) in
-  ({ uj_val  = mkCase (ci, nf_betaiota pj.uj_val, cj.uj_val,
+  ({ uj_val  = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
                        Array.map j_val lfj);
      uj_type = rslty },
   Constraint.union univ univ')
-- 
cgit v1.2.3