diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-15 10:03:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-15 10:03:21 +0000 |
| commit | 1cb6d3b235b03ccba046dee70b22d9f2e8dd8192 (patch) | |
| tree | 63019a4a21d95cb99dddcce7456e4f59d235771d /pretyping | |
| parent | ded45010b86ccc2203262f13340495b200f742bd (diff) | |
- Fixing bug #2139 (kernel-based test of well-formation of elimination
predicate called from proof refiner was failing because it was not
aware of evars instantiation; I added a nf_evar in 8.2 branch but for
the trunk, I propose to remove the elimination predicate
well-formation test; we therefore assume that tactics build correct
elimination predicates in Case, is it not too much demanding?).
- Seized the opportunity to remove dead kernel code about non dependent
elimination predicates (all predicates are stored dependent by
default since a few years now).
- Anecdotic complement to commit 12229 (removal of obsolete comment).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12241 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 15 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 1 |
3 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 8fe807f2e..14121d328 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -375,13 +375,16 @@ let set_pattern_names env ind brv = mip.mind_nf_lc in array_map2 (set_names env) arities brv - -let type_case_branches_with_names env indspec pj c = +let type_case_branches_with_names env indspec p c = let (ind,args) = indspec in - let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let params = list_firstn mib.mind_nparams args in - if is_elim_predicate_explicitly_dependent env pj.uj_val (ind,params) then + let (mib,mip as specif) = Inductive.lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let (params,realargs) = list_chop nparams args in + let lbrty = Inductive.build_branches_type ind specif params p in + (* Build case type *) + let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in + (* Adjust names *) + if is_elim_predicate_explicitly_dependent env p (ind,params) then (set_pattern_names env ind lbrty, conclty) else (lbrty, conclty) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5d416cede..357fb0908 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -104,7 +104,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - env -> inductive * constr list -> unsafe_judgment -> constr -> + env -> inductive * constr list -> constr -> constr -> types array * types val make_case_info : env -> inductive -> case_style -> case_info diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0846359a8..dcb5efae5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -97,7 +97,6 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst else error_cannot_unify_local env sigma (mkApp (f, l),c,c) | Evar ev -> - (* Currently unused: incompatible with eauto/eassumption backtracking *) sigma,metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst | _ -> assert false |