From 1bfd55b3ffc5d6bb710f1155bcac43cb3a3a35d0 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 29 Apr 2011 15:03:17 +0000 Subject: Some comments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14086 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/proof.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'proofs/proof.mli') diff --git a/proofs/proof.mli b/proofs/proof.mli index bb651dea1..eed0bc481 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -39,7 +39,7 @@ type proof val start : (Environ.env * Term.types) list -> proof -(* Returns [true] is the considered proof is completed, that is if no goal remain +(* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) val is_done : proof -> bool @@ -59,7 +59,11 @@ exception EmptyUndoStack val undo : proof -> unit (* Adds an undo effect to the undo stack. Use it with care, errors here might result - in inconsistent states. *) + in inconsistent states. + An undo effect is meant to undo an effect on a proof (a canonical example + of which is {!Proofglobal.set_proof_mode} which changes the current parser for + tactics). Make sure it will work even if the effects have been only partially + applied at the time of failure. *) val add_undo : (unit -> unit) -> proof -> unit (*** Focusing actions ***) -- cgit v1.2.3