diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -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 |