diff options
| author | herbelin | 2001-06-25 08:07:38 +0000 |
|---|---|---|
| committer | herbelin | 2001-06-25 08:07:38 +0000 |
| commit | 3c97ade2824232f1dbc800448f573796813f2611 (patch) | |
| tree | b4a1f1c389c22fcdb35a523e93443e9e6a8de536 | |
| 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
| -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 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 |