From 2a239725f493e643d0f26455293e6ca295f4dc92 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Thu, 14 Jun 2018 16:29:19 +0200
Subject: Workaround to handle non-value arguments in tactics.

Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
---
 test-suite/bugs/closed/2800.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
index 2ee438934e..54c75e344c 100644
--- a/test-suite/bugs/closed/2800.v
+++ b/test-suite/bugs/closed/2800.v
@@ -4,3 +4,16 @@ intuition
   match goal with
   | |- _ => idtac " foo"
   end.
+
+  lazymatch goal with _ => idtac end.
+  match goal with _ => idtac end.
+  unshelve lazymatch goal with _ => idtac end.
+  unshelve match goal with _ => idtac end.
+  unshelve (let x := I in idtac).
+Abort.
+
+Require Import ssreflect.
+
+Goal True.
+match goal with _ => idtac end => //.
+Qed.
-- 
cgit v1.2.3