From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 10:26:08 +0200 Subject: Remove some uses of Loadpath.get_paths. The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files. --- stm/vio_checking.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 4df9603dc..06bf955c8 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -104,9 +104,7 @@ let schedule_vio_compilation j fs = let f = if Filename.check_suffix f ".vio" then Filename.chop_extension f else f in - let paths = Loadpath.get_paths () in - let _, long_f_dot_v = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let long_f_dot_v = Loadpath.locate_file (f^".v") in let aux = Aux_file.load_aux_file_for long_f_dot_v in let eta = try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") -- cgit v1.2.3