2 files changed, 17 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e96e19015a..63e58c278f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -655,6 +655,19 @@ let give_up =
   Proof.set {initial with comb=[]} >>
   Proof.put (false,([],initial.comb))
 
+let cycle n =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  let l = List.length initial.comb in
+  let n' = n mod l in
+  (* if [n] is negative [n mod l] is negative of absolute value less
+     than [l], so [(n mod l)+l] is the representative of [n] in the
+     interval [[0,l-1]].*)
+  let n' = if n' < 0 then n'+l else n' in
+  let (front,rear) = List.chop n' initial.comb in
+  Proof.set {initial with comb=rear@front}
+
 (*** Commands ***)
 
 let in_proofview p k =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 8e47878fa2..fe732c4b37 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -266,6 +266,10 @@ val unshelve : Goal.goal list -> proofview -> proofview
    with given up goals cannot be closed. *)
 val give_up : unit tactic
 
+(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
+    is negative, then it puts the [n] last goals first.*)
+val cycle : int -> unit tactic
+
 exception Timeout
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)