diff options
Diffstat (limited to 'contrib/interface')
| -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 := |