diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 102 |
1 files changed, 55 insertions, 47 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index b19d8c04..a34446d8 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -886,11 +886,11 @@ let build_per_info etype casee gls = ET_Induction -> mind.mind_nparams_rec | _ -> mind.mind_nparams in let params,real_args = list_chop nparams args in - let abstract_obj body c = + let abstract_obj c body = let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in - let pred= List.fold_left abstract_obj - (lambda_create env (ctyp,subst_term casee concl)) real_args in + let pred= List.fold_right abstract_obj + real_args (lambda_create env (ctyp,subst_term casee concl)) in is_dep, {per_casee=casee; per_ctype=ctyp; @@ -1273,7 +1273,7 @@ end*) let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = - match tree with + match tree with Pop t -> let is_rec,nstacks = pop_stacks stacks in if is_rec then @@ -1309,51 +1309,59 @@ let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = kont] gls) end gls | Split(ids,ind,br) -> - let (_,typ,_)=destProd (pf_concl gls) in + let (_,typ,_)= + try destProd (pf_concl gls) with Invalid_argument _ -> + anomaly "Sub-object not found." in let hd,args=decompose_app (special_whd gls typ) in - let _ = assert (ind = destInd hd) in - let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in - let params = list_firstn nparams args in - let constr i =applist (mkConstruct(ind,succ i),params) in - let next_tac is_rec i = function - Some (sub_ids,tree) -> - let br_stacks = - List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in - let p_stacks = - push_head (constr i) is_rec ids br_stacks in - execute_cases false fix_name per_info kont0 p_stacks tree - | None -> - msgnl (str "Warning : missing case"); - kont0 (mkMeta 1) - in - let id = pf_get_new_id patvar_base gls in - let kont is_rec = - tclTHENSV - (general_case_analysis (mkVar id,NoBindings)) - (Array.mapi (next_tac is_rec) br) in - tclTHEN - (intro_mustbe_force id) - begin - match fix_name with - Anonymous -> kont false - | Name fix_id -> - (fun gls -> - if at_top then - kont false gls - else - match hrec_for id fix_id per_info gls with - None -> kont false gls - | Some c_obj -> - tclTHENLIST - [generalize [c_obj]; - kont true] gls) - end gls + if try ind <> destInd hd with Invalid_argument _ -> true then + (* argument of an inductive family : intro + discard *) + tclTHEN intro + (execute_cases at_top fix_name per_info kont0 stacks tree) gls + else + begin + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let params = list_firstn nparams args in + let constr i =applist (mkConstruct(ind,succ i),params) in + let next_tac is_rec i = function + Some (sub_ids,tree) -> + let br_stacks = + List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in + let p_stacks = + push_head (constr i) is_rec ids br_stacks in + execute_cases false fix_name per_info kont0 p_stacks tree + | None -> + msgnl (str "Warning : missing case"); + kont0 (mkMeta 1) + in + let id = pf_get_new_id patvar_base gls in + let kont is_rec = + tclTHENSV + (general_case_analysis (mkVar id,NoBindings)) + (Array.mapi (next_tac is_rec) br) in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont false + | Name fix_id -> + (fun gls -> + if at_top then + kont false gls + else + match hrec_for id fix_id per_info gls with + None -> kont false gls + | Some c_obj -> + tclTHENLIST + [generalize [c_obj]; + kont true] gls) + end gls + end | End_of_branch (id,nhyps) -> - match List.assoc id stacks with - [None,_,args] -> - let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in - kont0 (applist (mkVar id,List.rev_append args metas)) gls - | _ -> anomaly "wrong stack size" + match List.assoc id stacks with + [None,_,args] -> + let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in + kont0 (applist (mkVar id,List.rev_append args metas)) gls + | _ -> anomaly "wrong stack size" let end_tac et2 gls = let info = get_its_info gls in |