diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/ipat_swap.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/ssr/ipat_swap.v b/test-suite/ssr/ipat_swap.v index 9ca7f256dc..1d78a2a009 100644 --- a/test-suite/ssr/ipat_swap.v +++ b/test-suite/ssr/ipat_swap.v @@ -2,7 +2,7 @@ Require Import ssreflect. Section Swap. -Variable P : nat -> bool. +Definition P n := match n with 1 => true | _ => false end. Lemma test_swap1 : forall (n : nat) (b : bool), P n = b. Proof. move=> /[swap] b n; suff: P n = b by []. Abort. |