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 +-
 test-suite/success/Hints.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

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
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 036ba034dd..f32753e023 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -17,9 +17,9 @@ Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal.
 Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo.
 
 (* What's this stranged syntax ? *)
-HintDestruct Conclusion h6 (le ? ?) 4 [ (Apply $0) ].
-HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ (Apply $0) ].
-HintDestruct Hypothesis h8 (le ? ?) 4 [ (Apply $0) ].
+HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ].
+HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ].
+HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ].
 
 (* Checks that local names are accepted *)
 Section A.
-- 
cgit v1.2.3