From 8ded09eb5e1c28d8a6630c7d3e6d93f2ef4270be Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 5 Jun 2002 14:43:35 +0000
Subject: Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct

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

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 78294f2a71..9f5ef5c8be 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -90,7 +90,7 @@ GEXTEND Gram
           id  = ident;
           hyptyp = Constr.constr_pattern;
           pri = natural;
-          tac = tactic -> 
+          "["; tac = tactic; "]" -> 
 	    VernacHintDestruct (id,dloc,hyptyp,pri,tac)
 
       | IDENT "Hint"; hintname = ident; dbnames = opt_hintbases; ":="; h = hint
-- 
cgit v1.2.3