From a4dce1658f9a946cedb40ddcf0cdbc5391dd2005 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 29 Nov 2017 14:49:14 +0100 Subject: Forbid implicitly relative names in the checker. Before this patch, passing a mere identifier (without dots) to the checker would make it consider it as implicitly referring to a relative name. For instance, if passed "foo", it would have looked for "Bar.foo.vo" and "Qux.foo.vo" if those files were in the loadpath. This was quite ad-hoc. We remove this "feature" and require the user to always give either a filename or a fully qualified logical name. --- checker/check.ml | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 21fdba1fa..a00ec3b0e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -129,8 +129,6 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -let get_load_paths () = fst !load_paths - (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) @@ -227,13 +225,8 @@ let locate_absolute_library dir = let locate_qualified_library qid = try - let loadpath = - (* Search library in loadpath *) - if qid.dirpath=[] then get_load_paths () - else - (* we assume qid is an absolute dirpath *) - load_paths_of_dir_path (dir_of_path qid) - in + (* we assume qid is an absolute dirpath *) + let loadpath = load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in let path, file = System.where_in_path loadpath name in -- cgit v1.2.3