From f39a711555d76926b6e0ddf5480a6411abc862a9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 23 Jun 2015 16:59:08 +0200
Subject: Fixing incompatibility introduced with simpl in commit 364decf59c1
 (or maybe ca71714).

Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.

was working in 8.4 but was failing in 8.5beta2.

Note: Changes in tacintern.ml are otherwise purely cosmetic.
---
 test-suite/success/simpl.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index e540ae5f30..5b87e877bf 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *)
 simpl (unbox _ (unbox _ _)) at 2 4.
 match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end.
 Abort.
+
+(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *)
+
+Goal 2=1+1.
+match goal with |- (_ = ?c) => simpl c end.
+match goal with |- 2 = 2 => idtac end. (* Check that it reduced *)
+Abort.
-- 
cgit v1.2.3