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/interface/blast.ml | |
| 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/interface/blast.ml')
| -rw-r--r-- | contrib/interface/blast.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 := |