diff options
| author | herbelin | 2011-10-29 11:59:11 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-29 11:59:11 +0000 |
| commit | 62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (patch) | |
| tree | e4d7d609af1b03ffa12b7c7c0ce4e08ea06303ca /toplevel | |
| parent | 97da8221e0097ed365f0a99e4960148424a59734 (diff) | |
Added checksums to glob files and warned about possibly missing
packages for utf8.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 87e0ebe17a..934cddb4f8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -307,15 +307,14 @@ 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 = Flags.verbosely Library.start_library f in - if Dumpglob.multi_dump () then - Dumpglob.open_glob_file (f ^ ".glob"); - Dumpglob.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 Dumpglob.multi_dump () then Dumpglob.close_glob_file (); - Library.save_library_to ldir (long_f_dot_v ^ "o") + Dumpglob.start_dump_glob long_f_dot_v; + Dumpglob.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 (); + Dumpglob.end_dump_glob (); + Library.save_library_to ldir (long_f_dot_v ^ "o") |