Fixing [dup] and [swap]

4 files changed, 49 insertions, 28 deletions

diff --git a/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst
new file mode 100644
index 0000000000..e14ae89219
--- /dev/null
+++ b/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Working around a bug of interaction between + and /(ltac:(...)) cf #13458
+  (`#13459 <https://github.com/coq/coq/pull/13459>`_,
+  by Cyril Cohen).
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.
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index dc81b5cca7..db572d25d8 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -671,43 +671,32 @@ Module Export ipat.
 Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
   (at level 0, only parsing) : ssripat_scope.
 
-(** We try to preserve the naming by matching the names from the goal.
-    We do 'move' to perform a hnf before trying to match.               **)
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match                *)
 Notation "'[' 'swap' ']'" := (ltac:(move;
-  lazymatch goal with
-  | |- forall (x : _), _ => let x := fresh x in move=> x; move;
-    lazymatch goal with
-    | |- forall (y : _), _ => let y := fresh y in move=> y; move: y x
-    | |- let y := _ in _ => let y := fresh y in move=> y; move: @y x
-    | _ => let y := fresh "_top_" in move=> y; move: y x
-    end
-  | |- let x := _ in _ => let x := fresh x in move => x; move;
-    lazymatch goal with
-    | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
-    | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
-    | _ => let y := fresh "_top_" in move=> y; move: y x
-    end
-  | _ => let x := fresh "_top_" in let x := fresh x in move=> x; move;
-    lazymatch goal with
-    | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
-    | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
-    | _ => let y := fresh "_top_" in move=> y; move: y x
-    end
-  end))
+  let x := lazymatch goal with
+    | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_"
+  end in intro x; move;
+  let y := lazymatch goal with
+    | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_"
+  end in intro y; revert x; revert y))
   (at level 0, only parsing) : ssripat_scope.
 
+
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match                *)
 Notation "'[' 'dup' ']'" := (ltac:(move;
   lazymatch goal with
   | |- forall (x : _), _ =>
-    let x := fresh x in move=> x;
-    let copy := fresh x in have copy := x; move: copy x
+    let x := fresh x in intro x;
+    let copy := fresh x in have copy := x; revert x; revert copy
   | |- let x := _ in _ =>
-    let x := fresh x in move=> x;
+    let x := fresh x in intro x;
     let copy := fresh x in pose copy := x;
-    do [unfold x in (value of copy)]; move: @copy @x
+    do [unfold x in (value of copy)]; revert x; revert copy
   | |- _ =>
     let x := fresh "_top_" in move=> x;
-    let copy := fresh "_top" in have copy := x; move: copy x
+    let copy := fresh "_top" in have copy := x; revert x; revert copy
   end))
   (at level 0, only parsing) : ssripat_scope.