From 3c97ade2824232f1dbc800448f573796813f2611 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Jun 2001 08:07:38 +0000
Subject: Bug dépendances non pertinentes (dû à des K-rédex) dans le type des
 branches des Cases non contournées (bug Solange Coupet)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1801 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4ab877bdaf..038f70c2c2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -790,6 +790,11 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
   if Array.length cstrs = 0 then (* "TODO4-3" *)
     error "Inference of annotation for empty inductive types not implemented"
   else
+    (* Empiric normalization: p may depend in a irrelevant way on args of the*)
+    (* cstr as in [c:{_:Alpha & Beta}] Cases c of (existS a b)=>(a,b) end *)
+    let typs =
+      Array.map (local_strong (whd_betaevar empty_env (evars_of isevars))) typs
+    in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
     let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
-- 
cgit v1.2.3