diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 2301d8a0d..08f9a279d 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -59,9 +59,11 @@ val is_unsafe : string -> bool (* Dump of globalization (to be used by coqdoc) *) +val noglob : bool ref val dump : bool ref val dump_into_file : string -> unit val dump_string : string -> unit +val dump_it : unit -> unit (* Options for the virtual machine *) |