From 208f162ab68d00488248ee052947592dd23d5d52 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 14 Mar 2009 21:29:19 +0000
Subject: 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
---
 contrib/interface/blast.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'contrib/interface')

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 :=
-- 
cgit v1.2.3