diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 08:07:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 08:07:38 +0000 |
| commit | 3c97ade2824232f1dbc800448f573796813f2611 (patch) | |
| tree | b4a1f1c389c22fcdb35a523e93443e9e6a8de536 /pretyping/cases.ml | |
| parent | 1618dc59f8d1a7cf27bbae9ee08a2cd8f4cc5d35 (diff) | |
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
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |