From 9205d8dc7b9e97b6c2f0815fddc5673c21d11089 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 2 Nov 2015 12:26:53 +0100
Subject: Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in
 WG.

---
 test-suite/bugs/closed/3682.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/bugs/closed/3682.v')

diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v
index 2a282d221f..9d37d1a2d0 100644
--- a/test-suite/bugs/closed/3682.v
+++ b/test-suite/bugs/closed/3682.v
@@ -3,4 +3,4 @@ Class Foo.
 Definition bar `{Foo} (x : Set) := Set.
 Instance: Foo.
 Definition bar1 := bar nat.
-Definition bar2 := bar $(admit)$.
+Definition bar2 := bar ltac:(admit).
-- 
cgit v1.2.3