Some comments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14086 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 7 insertions, 2 deletions

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 ***)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 5f57c25ac..e32ec85ad 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -21,6 +21,7 @@ type proof_mode = {
   set : unit -> unit ;
   reset : unit -> unit
 }
+
 (** Registers a new proof mode which can then be adressed by name
     in [set_default_proof_mode].
     One mode is already registered - the standard mode - named "No",