From d2d23987680f1328e91e57d93bef875766455cff Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Jul 2014 18:16:24 +0200
Subject: Add a tactic [swap i j] to swap the position of goals [i] and [j].

If [i] or [j] is negative goals are counted from the end.---
 tactics/extratactics.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 635904cc7e..d0993b66ea 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -876,3 +876,8 @@ END
 TACTIC EXTEND cycle
 | [ "cycle" int_or_var(n) ] -> [ Proofview.cycle (out_arg n) ]
 END
+
+(* swaps goals number [i] and [j] *)
+TACTIC EXTEND swap
+| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap (out_arg i) (out_arg j) ]
+END
-- 
cgit v1.2.3