From fd47b2d2638518fe62ce9c63557d2dab219d9558 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Thu, 30 Jun 2016 19:41:53 +0200
Subject: Goal selectors now use the keyword [only].

This fixes some parsing problems when doing things like
[let n := 2 in idtac n]. See bug #4877.
---
 test-suite/bugs/closed/4877.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/closed/4877.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v
new file mode 100644
index 0000000000..7e3c78dc2e
--- /dev/null
+++ b/test-suite/bugs/closed/4877.v
@@ -0,0 +1,12 @@
+Ltac induction_last :=
+  let v := match goal with
+           | |- forall x y, _ = _ -> _ => 1
+           | |- forall x y, _ -> _ = _ -> _ => 2
+           | |- forall x y, _ -> _ -> _ = _ -> _ => 3
+           end in
+  induction v.
+
+Goal forall n m : nat, True -> n = m -> m = n.
+  induction_last.
+  reflexivity.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3