diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 4cab303815..8c16e5b858 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -57,11 +57,6 @@ val print_hyps_limit : unit -> int option val add_unsafe : string -> unit val is_unsafe : string -> bool -(* Dump of globalization (to be used by coqdoc) *) - -val noglob : bool ref -val dump : bool ref - (* Options for the virtual machine *) val set_boxed_definitions : bool -> unit |