diff options
| -rw-r--r-- | proofs/proof.mli | 8 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 1 |
2 files changed, 7 insertions, 2 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index bb651dea11..eed0bc481a 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 5f57c25ac5..e32ec85ad9 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", |