aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-07-15 10:03:21 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-07-15 10:03:21 +0000
commit1cb6d3b235b03ccba046dee70b22d9f2e8dd8192 (patch)
tree63019a4a21d95cb99dddcce7456e4f59d235771d
parentded45010b86ccc2203262f13340495b200f742bd (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
-rw-r--r--kernel/inductive.ml29
-rw-r--r--kernel/inductive.mli4
-rw-r--r--pretyping/inductiveops.ml15
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/unification.ml1
-rw-r--r--proofs/logic.ml3
6 files changed, 26 insertions, 28 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8024ae266..23cd99d1e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -308,10 +308,7 @@ let is_correct_arity env c pj ind specif params =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
check_allowed_sort ksort specif;
- (true, Constraint.union u univ)
- | Sort s', [] ->
- check_allowed_sort (family_of_sort s') specif;
- (false, u)
+ Constraint.union u univ
| _ ->
raise (LocalArity None)
in
@@ -325,38 +322,34 @@ let is_correct_arity env c pj ind specif params =
(* [p] is the predicate, [i] is the constructor number (starting from 0),
and [cty] is the type of the constructor (params not instantiated) *)
-let build_branches_type ind (_,mip as specif) params dep p =
+let build_branches_type ind (_,mip as specif) params p =
let build_one_branch i cty =
let typi = full_constructor_instantiate (ind,specif,params) cty in
let (args,ccl) = decompose_prod_assum typi in
let nargs = rel_context_length args in
let (_,allargs) = decompose_app ccl in
let (lparams,vargs) = list_chop (inductive_params specif) allargs in
- let cargs =
- if dep then
- let cstr = ith_constructor_of_inductive ind (i+1) in
- let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
- vargs @ [dep_cstr]
- else
- vargs in
+ let cargs =
+ let cstr = ith_constructor_of_inductive ind (i+1) in
+ let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
+ vargs @ [dep_cstr] in
let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
it_mkProd_or_LetIn base args in
Array.mapi build_one_branch mip.mind_nf_lc
(* [p] is the predicate, [c] is the match object, [realargs] is the
list of real args of the inductive type *)
-let build_case_type dep p c realargs =
- let args = if dep then realargs@[c] else realargs in
- beta_appvect p (Array.of_list args)
+let build_case_type p c realargs =
+ beta_appvect p (Array.of_list (realargs@[c]))
let type_case_branches env (ind,largs) pj c =
let specif = lookup_mind_specif env ind in
let nparams = inductive_params specif in
let (params,realargs) = list_chop nparams largs in
let p = pj.uj_val in
- let (dep,univ) = is_correct_arity env c pj ind specif params in
- let lc = build_branches_type ind specif params dep p in
- let ty = build_case_type dep p c realargs in
+ let univ = is_correct_arity env c pj ind specif params in
+ let lc = build_branches_type ind specif params p in
+ let ty = build_case_type p c realargs in
(lc, ty, univ)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d09cdbdb7..f877b5391 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -65,6 +65,10 @@ val type_case_branches :
env -> inductive * constr list -> unsafe_judgment -> constr
-> types array * types * constraints
+val build_branches_type :
+ inductive -> mutual_inductive_body * one_inductive_body ->
+ constr list -> constr -> types array
+
(* Return the arity of an inductive type *)
val mind_arity : one_inductive_body -> rel_context * sorts_family
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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8ba88185..f1f33930e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -436,12 +436,11 @@ and mk_casegoals sigma goal goalacc p c =
let env = evar_env goal in
let (acc',ct) = mk_hdgoals sigma goal goalacc c in
let (acc'',pt) = mk_hdgoals sigma goal acc' p in
- let pj = {uj_val=p; uj_type=pt} in
let indspec =
try find_mrectype env sigma ct
with Not_found -> anomaly "mk_casegoals" in
let (lbrty,conclty) =
- type_case_branches_with_names env indspec pj c in
+ type_case_branches_with_names env indspec p c in
(acc'',lbrty,conclty)