diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 931fc1ca40..b020f89457 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -45,10 +45,10 @@ let dump_string s = if dump () && !glob_output != Feedback then Pervasives.output_string !glob_file s -let start_dump_glob vfile = +let start_dump_glob ~vfile ~vofile = match !glob_output with | MultFiles -> - open_glob_file (Filename.chop_extension vfile ^ ".glob"); + open_glob_file (Filename.chop_extension vofile ^ ".glob"); output_string !glob_file "DIGEST "; output_string !glob_file (Digest.to_hex (Digest.file vfile)); output_char !glob_file '\n' @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir |