From ff74451389c13828c644157c960c0d314b389b95 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 19 Sep 2018 16:58:36 +0200
Subject: [ssr] use the right environment in ssrpattern (fix #8454)

---
 test-suite/ssr/ssrpattern.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/ssr/ssrpattern.v

(limited to 'test-suite')

diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v
new file mode 100644
index 0000000000..422bb95fdf
--- /dev/null
+++ b/test-suite/ssr/ssrpattern.v
@@ -0,0 +1,7 @@
+Require Import ssrmatching.
+
+Goal forall n, match n with 0 => 0 | _ => 0 end = 0.
+Proof.
+  intro n.
+  ssrpattern (match _ with 0 => _ | S n' => _ end).
+Abort.
-- 
cgit v1.2.3