diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-18 15:58:12 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-18 15:58:12 +0000 |
| commit | d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa (patch) | |
| tree | 589b400e1a0416b49150ae669ea0ff6cfacbd605 /lib/flags.ml | |
| parent | ccff0b020b3a0950a6358846b6a40b8cd7a96562 (diff) | |
Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from de coqdoc (compatibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index f2ab87b4b..4743345de 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 |