diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 13 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 3 |
2 files changed, 5 insertions, 11 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 7f0632bd7c..1042061021 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2617,13 +2617,10 @@ let dirpath_of_file f = let new_doc { doc_type ; iload_path; require_libs; stm_options } = - let load_objs libs = - let rq_file (dir, from, exp) = - let mp = Libnames.qualid_of_string dir in - let mfrom = Option.map Libnames.qualid_of_string from in - Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - List.(iter rq_file (rev libs)) - in + let require_file (dir, from, exp) = + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2662,7 +2659,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = end; (* Import initial libraries. *) - load_objs require_libs; + List.iter require_file require_libs; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index fab6767beb..baa7b3570c 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -11,7 +11,6 @@ open Util let check_vio (ts,f_in) = - Dumpglob.noglob (); let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -142,5 +141,3 @@ let schedule_vio_compilation j fs = List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - |