diff options
| -rw-r--r-- | proofs/proofview.ml | 13 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 5 |
3 files changed, 22 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index e96e19015..63e58c278 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 8e47878fa..fe732c4b3 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]. *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index fa2ac3712..635904cc7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -871,3 +871,8 @@ TACTIC EXTEND give_up | [ "give_up" ] -> [ Proofview.give_up ] END + +(* cycles [n] goals *) +TACTIC EXTEND cycle +| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle (out_arg n) ] +END |