Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bug

Reviewed-by: gares

2 files changed, 29 insertions, 1 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.
diff --git a/test-suite/ssr/ipat_swap.v b/test-suite/ssr/ipat_swap.v
index 1d78a2a009..a06dae1264 100644
--- a/test-suite/ssr/ipat_swap.v
+++ b/test-suite/ssr/ipat_swap.v
@@ -7,7 +7,19 @@ 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.
 
-Lemma test_swap1 : let n := 1 in let b := true in False.
+Lemma test_swap2 : let n := 1 in let b := true in False.
 Proof. move=> /[swap] b n; have : P n = b := eq_refl. Abort.
 
+Lemma test_swap_plus P Q R : P -> Q -> R -> False.
+Proof.
+move=> + /[swap].
+suff: P -> R -> Q -> False by [].
+Abort.
+
+Lemma test_swap_plus2 P : P -> let x := 0 in let y := 1 in False.
+Proof.
+move=> + /[swap].
+suff: P -> let y := 1 in let x := 0 in False by [].
+Abort.
+
 End Swap.