2 files changed, 9 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 48ca84891..7cdfacadb 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 72dcc8c37..ae18934e7 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