diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 9 | ||||
| -rw-r--r-- | lib/flags.mli | 5 |
2 files changed, 2 insertions, 12 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index f2ab87b4b7..4743345de7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -82,18 +82,13 @@ let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set -(* Dump of globalization (to be used by coqdoc) *) - -let noglob = ref false -let dump = ref false - -(* Flags.for the virtual machine *) +(* Flags for the virtual machine *) let boxed_definitions = ref true let set_boxed_definitions b = boxed_definitions := b let boxed_definitions _ = !boxed_definitions -(* Flags.for external tools *) +(* Flags for external tools *) let subst_command_placeholder s t = let buff = Buffer.create (String.length s + String.length t) in 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 |