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/vio_checking.ml') diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 4df9603dca..06bf955c82 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 From 315aac9ae0d411c10849c421d5dfd8e134919233 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Dec 2015 11:30:35 +0100 Subject: vio: fix argument parsing (progress on #4442) --- stm/vio_checking.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/vio_checking.ml') diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 06bf955c82..ce930cacb7 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -43,7 +43,7 @@ let schedule_vio_checking j fs = let rec filter_argv b = function | [] -> [] | "-schedule-vio-checking" :: rest -> filter_argv true rest - | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) + | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) | _ :: rest when b -> filter_argv b rest | s :: rest -> s :: filter_argv b rest in let pack = function -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- stm/vio_checking.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/vio_checking.ml') diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index ce930cacb7..d4dcf72c13 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*