test-suite/ssr/ssrpattern.v


1
2
3
4
5
6
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.