Merge pull request #672 from CohenCyril/fix_dup_swap

Fixing [dup] and [swap] for Coq 8.12

1 files changed, 11 insertions, 25 deletions

diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 888f98d..e1e1b71 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -111,26 +111,12 @@ Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
 (* 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 *)
@@ -138,15 +124,15 @@ Notation "'[' 'swap' ']'" := (ltac:(move;
 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.