diff options
| author | herbelin | 2009-03-14 21:29:19 +0000 |
|---|---|---|
| committer | herbelin | 2009-03-14 21:29:19 +0000 |
| commit | 208f162ab68d00488248ee052947592dd23d5d52 (patch) | |
| tree | 4009b4e1da390933e5ccfc878390478041c6679a /contrib | |
| parent | 4b7200cbbf4f2462d6f1398a191377b4d57f7655 (diff) | |
Cleaning/uniformizing the interface of tacticals.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 6 | ||||
| -rw-r--r-- | contrib/funind/recdef.ml | 6 | ||||
| -rw-r--r-- | contrib/interface/blast.ml | 6 |
3 files changed, 9 insertions, 9 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 75b811d518..adfb9ce2ff 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1015,7 +1015,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = (tclDO nb_intro_to_do intro) ( fun g' -> - let just_introduced = nLastHyps nb_intro_to_do g' in + let just_introduced = nLastDecls nb_intro_to_do g' in let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g' ) @@ -1218,7 +1218,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : [ (* observe_tac ("introducing args") *) (tclDO nb_args intro); (fun g -> (* replacement of the function by its body *) - let args = nLastHyps nb_args g in + let args = nLastDecls nb_args g in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) let args_id = List.map (fun (id,_,_) -> id) args in @@ -1282,7 +1282,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : [ tclDO nb_args intro; (fun g -> (* replacement of the function by its body *) - let args = nLastHyps nb_args g in + let args = nLastDecls nb_args g in let args_id = List.map (fun (id,_,_) -> id) args in let dyn_infos = { diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index 100868a0e5..aee133f6d9 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -769,9 +769,9 @@ let termination_proof_header is_mes input_type ids args_id relation (* rest of the proof *) tclTHENSEQ [observe_tac "generalize" - (onNLastHyps (nargs+1) - (fun (id,_,_) -> - tclTHEN (h_generalize [mkVar id]) (h_clear false [id]) + (onNLastHypsId (nargs+1) + (tclMAP (fun id -> + tclTHEN (h_generalize [mkVar id]) (h_clear false [id])) )) ; observe_tac "h_fix" (h_fix (Some hrec) (nargs+1)); diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 483453cb30..17020c46d0 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -519,15 +519,15 @@ let blast_simpl = (free_try (reduce (Simpl None) onConcl)) ;; let blast_induction1 = (free_try (tclTHEN (tclTRY intro) - (tclTRY (tclLAST_HYP simplest_elim)))) + (tclTRY (onLastHyp simplest_elim)))) ;; let blast_induction2 = (free_try (tclTHEN (tclTRY (tclTHEN intro intro)) - (tclTRY (tclLAST_HYP simplest_elim)))) + (tclTRY (onLastHyp simplest_elim)))) ;; let blast_induction3 = (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro))) - (tclTRY (tclLAST_HYP simplest_elim)))) + (tclTRY (onLastHyp simplest_elim)))) ;; blast_tactic := |