diff options
| author | Maxime Dénès | 2018-09-26 15:39:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 15:39:09 +0200 |
| commit | 3f486b2334fa3a5ab7774e212a5c592ba241535c (patch) | |
| tree | 35e9ec7cff5a560771668fee993e4dc4cd049091 /test-suite | |
| parent | 6a48e732577b9ab09d458c7526f599d4528fe2fc (diff) | |
| parent | ff74451389c13828c644157c960c0d314b389b95 (diff) | |
Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/ssrpattern.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |