diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-18 13:29:27 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-18 13:29:27 +0000 |
| commit | 29d09a8e15ae7c1e88821f3d662ad845338c0013 (patch) | |
| tree | 5d1b0355bfc5f39a28604519a9b332796669ed79 /tactics | |
| parent | 8c23671d5a8bf6a5c197bbcaec1af2084d654ed3 (diff) | |
debug plus poussé induction dépendante
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9787 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index ac33ba61a..4c526ecee 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -882,11 +882,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; @@ -1298,9 +1298,11 @@ 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 - if ind <> destInd hd then + 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 |