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.

1 files changed, 1 insertions, 3 deletions

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")