From 162c8ec86c428e8de7d3275e39eb5ac3a3413267 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 3 May 2000 20:49:18 +0000
Subject: Reparation du bug d'interpretation d'Abstract

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@409 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b21ac1825b..98a732287e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1680,9 +1680,9 @@ let tclABSTRACT name_op tac gls =
 
 let dyn_tclABSTRACT = 
   hide_tactic "ABSTRACT"
-    (function 
-       | [Tacexp tac] -> 
-	   tclABSTRACT None (Tacinterp.interp tac)
-       | [Identifier s; Tacexp tac] -> 
-	   tclABSTRACT (Some s) (Tacinterp.interp tac)
-       | _ -> invalid_arg "tclABSTRACT")
+   (function 
+       | [Tac tac] ->
+	   tclABSTRACT None tac
+       | [Identifier s; Tac tac] ->
+	   tclABSTRACT (Some s) tac
+       | _ -> invalid_arg "tclABSTRACT") 
-- 
cgit v1.2.3