diff options
| author | Cyril Cohen | 2020-11-08 00:22:53 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-08 00:22:53 +0100 |
| commit | 7bd93b0d6000766d766da4a73dbe44e4189b2085 (patch) | |
| tree | 4be59faa4058932d49f83cf10b46c53e952942af | |
| parent | 54c3b4939e975205b93617e2357014bf95583551 (diff) | |
fixup
| -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. |