diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index eed0bc481..cbde9244a 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -129,6 +129,18 @@ val with_end_tac : proof -> unit Proofview.tactic -> unit Proofview.tactic val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit +(*** Transactions ***) + +(* A transaction chains several commands into a single one. For instance, + a focusing command and a tactic. Transactions are such that if + any of the atomic action fails, the whole transaction fails. + + During a transaction, the undo visible undo stack is constituted only + of the actions performed done during the transaction. + + [transaction p f] can be called on an [f] using, itself, [transaction p].*) +val transaction : proof -> (unit -> unit) -> unit + (*** Compatibility layer with <=v8.2 ***) module V82 : sig val subgoals : proof -> Goal.goal list Evd.sigma |