diff options
| -rw-r--r-- | kernel/inductive.ml | 29 | ||||
| -rw-r--r-- | kernel/inductive.mli | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 15 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 1 | ||||
| -rw-r--r-- | proofs/logic.ml | 3 |
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) |