diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-29 15:03:25 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-29 15:03:25 +0000 |
| commit | d10841e20af67563b60d7cf91e251079b35b6636 (patch) | |
| tree | 5b3b2631b68b374eed85c93379ba081c790b4d3a /proofs/proof.mli | |
| parent | 1bfd55b3ffc5d6bb710f1155bcac43cb3a3a35d0 (diff) | |
Fixed a bug causing inconsistent states during proof editting.
Some toplevel commands (for instance the experimental bullets) are
composed of several atomic commands, the failure of one must imply
the failure of the whole toplevel command. This commit introduces
a system of transaction to that effect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14087 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |