1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
index 2ee43893..54c75e34 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.