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) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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(+) (limited to 'pretyping/cases.ml') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4ab877bda..038f70c2c 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