From d7072a91a9c40cf9a9cc6e6cdd087f925e591aec Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 8 Sep 2014 09:29:20 +0200
Subject: Add a tactic [revgoals] to reverse the list of focused goals.

---
 tactics/extratactics.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c90ec92d2b..4498c3197b 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -891,6 +891,11 @@ TACTIC EXTEND swap
 | [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap (out_arg i) (out_arg j) ]
 END
 
+(* reverses the list of focused goals *)
+TACTIC EXTEND revgoals
+| [ "revgoals" ] -> [ Proofview.revgoals ]
+END
+
 
 type cmp =
   | Eq
-- 
cgit v1.2.3