From 00e25f45a58663515dbd624c4ea636d55dcd685b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 10 Sep 2005 17:20:12 +0000
Subject: Petit bug Declare Implicit Tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7370 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c2f3c25c1c..3cc73e21d5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -429,7 +429,7 @@ VERNAC COMMAND EXTEND AddStepr
     [ add_transitivity_lemma false t ]
 END
 
-VERNAC COMMAND EXTEND AddStepr
+VERNAC COMMAND EXTEND ImplicitTactic
 | [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
     [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ]
 END
-- 
cgit v1.2.3