diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-29 15:03:17 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-29 15:03:17 +0000 |
| commit | 1bfd55b3ffc5d6bb710f1155bcac43cb3a3a35d0 (patch) | |
| tree | 5524debe021614b6a058eb57a3cb7213ab592201 /proofs/proof_global.mli | |
| parent | c9bab9479166334c633e41def7e2b724a3773e30 (diff) | |
Some comments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14086 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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", |