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.

---
 proofs/proofview.ml      | 6 ++++++
 proofs/proofview.mli     | 3 +++
 tactics/extratactics.ml4 | 5 +++++
 3 files changed, 14 insertions(+)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 48ca848915..7cdfacadb2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -692,6 +692,12 @@ let swap i j =
   in
   Proof.set {initial with comb}
 
+let revgoals =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  Proof.set {initial with comb=List.rev initial.comb}
+
 let numgoals =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 72dcc8c375..ae18934e71 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -287,6 +287,9 @@ val cycle : int -> unit tactic
     [1] as well, rather than raising an error. *)
 val swap : int -> int -> unit tactic
 
+(** [revgoals] reverse the list of focused goals. *)
+val revgoals : unit tactic
+
 (** [numgoals] returns the number of goals under focus. *)
 val numgoals : int tactic
 
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