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
---
 test-suite/success/Hints.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

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