From d10841e20af67563b60d7cf91e251079b35b6636 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 29 Apr 2011 15:03:25 +0000 Subject: 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 --- proofs/proof.mli | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'proofs/proof.mli') 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 -- cgit v1.2.3