diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-21 14:13:32 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-21 14:13:32 +0000 |
| commit | 78fb07846e6ca303417699d19beaeaf1a97f96af (patch) | |
| tree | e9056e481fc8d36846408794aacabee70e74f76b /toplevel | |
| parent | 7cb292a84437289d1e4f5a6c7a50fe5e7e763ec8 (diff) | |
Begin-End Silent deviennent Set?Unset Silent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@899 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 780ef6dc3..f60ecbd3e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -30,6 +30,7 @@ open Printer open Tacinterp open Tactic_debug open Command +open Goptions (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *) let join_binders binders = @@ -659,6 +660,12 @@ let _ = (fun () -> mSG(print_sec_context_typ (string_of_id id))) | _ -> bad_vernac_args "PrintSec") +let _ = declare_async_bool_option + {optasyncname = "Silent"; + optasynckey = (PrimaryTable "Silent"); + optasyncread = is_silent; + optasyncwrite = make_silent } + let _ = add "BeginSilent" (function |