diff options
Diffstat (limited to 'test-suite/ssr/ipat_dup.v')
| -rw-r--r-- | test-suite/ssr/ipat_dup.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/ssr/ipat_dup.v b/test-suite/ssr/ipat_dup.v index b1936df31d..61666959c4 100644 --- a/test-suite/ssr/ipat_dup.v +++ b/test-suite/ssr/ipat_dup.v @@ -2,6 +2,8 @@ Require Import ssreflect. Section Dup. +Section withP. + Variable P : nat -> Prop. Lemma test_dup1 : forall n : nat, P n. @@ -10,4 +12,18 @@ Proof. move=> /[dup] m n; suff: P n by []. Abort. Lemma test_dup2 : let n := 1 in False. Proof. move=> /[dup] m n; have : m = n := eq_refl. Abort. +End withP. + +Lemma test_dup_plus P Q : P -> Q -> False. +Proof. +move=> + /[dup] q. +suff: P -> Q -> False by []. +Abort. + +Lemma test_dup_plus2 P : P -> let x := 0 in False. +Proof. +move=> + /[dup] y. +suff: P -> let x := 0 in False by []. +Abort. + End Dup. |