diff options
author | 2008-06-24 11:41:12 +0000 | |
---|---|---|
committer | 2008-06-24 11:41:12 +0000 | |
commit | 4823449f7f3800835bfd5ebc4de5bdf407fdc2c2 (patch) | |
tree | aea77208ed5b783f4f00c5c6679f1b1bdbbab264 /toplevel/vernac.ml | |
parent | de45178c0b684a211fa61866e82b045f12f85ffe (diff) |
Suppression de l'option -dump-glob et ajout d'une option -no-glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r-- | toplevel/vernac.ml | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ac834b2a5..c0ec55228 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -226,11 +226,17 @@ let load_vernac verb file = (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = let ldir,long_f_dot_v = Library.start_library f in - if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); - if !Flags.xml_export then !xml_start_library (); - let _ = load_vernac verbosely long_f_dot_v in - if Pfedit.get_all_proof_names () <> [] then - (message "Error: There are pending proofs"; exit 1); - if !Flags.xml_export then !xml_end_library (); - Library.save_library_to ldir (long_f_dot_v ^ "o") + let dumpstate = !Flags.dump in + if not !Flags.noglob then + (Flags.dump_into_file (f ^ ".glob"); + Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n")); + if !Flags.xml_export then !xml_start_library (); + let _ = load_vernac verbosely long_f_dot_v in + if Pfedit.get_all_proof_names () <> [] then + (message "Error: There are pending proofs"; exit 1); + if !Flags.xml_export then !xml_end_library (); + if !Flags.dump then Flags.dump_it (); + Flags.dump := dumpstate; + Library.save_library_to ldir (long_f_dot_v ^ "o") + |