From 45aeeae98cca32fb474fba4d36c529a50f90a16b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 Feb 2008 18:05:31 +0000
Subject: Granting wish 1794 (the name provided in the "using" clause of the
 "abstract" tactical is now as a regular ltac parameter of the "identifier"
 type).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10549 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a403832fff..24149a98e7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1589,7 +1589,9 @@ and eval_tactic ist = function
   | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
   | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
-  | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
+  | TacAbstract (tac,ido) ->
+      fun gl -> Tactics.tclABSTRACT
+        (Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl
   | TacThen (t1,tf,t,tl) -> 
       tclTHENS3PARTS (interp_tactic ist t1)
 	(Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
-- 
cgit v1.2.3