From 97fba91264669d495643f6a3de6a09790ae2a1da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 21:08:12 +0200
Subject: Continuing 817308ab (use ltac env for terms in ltac context) + fix of
 syntax in test file ltac.v.

---
 test-suite/success/ltac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 952f35bc35..f9df021dc2 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -304,5 +304,5 @@ Abort.
 Goal True.
 let x := ipattern:y in assert (forall x y, x = y + 0).
 intro.
-destruct y. (* Check that the name is y here *).
+destruct y. (* Check that the name is y here *)
 Abort.
-- 
cgit v1.2.3