diff options
| author | Maxime Dénès | 2017-12-07 10:37:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-07 10:37:18 +0100 |
| commit | c8f6903de4d9debb3fe38755a3f5e7b558a014e2 (patch) | |
| tree | a3fcda963f4c448b3a56b17cb4c861acdbd4ab61 /checker/check.ml | |
| parent | f6751c59467e3a25f9318a1f8b74f768924f4892 (diff) | |
| parent | 9c0f36adac233efb1164ef88c86c78c7509d8b2c (diff) | |
Merge PR #6277: Qualified import in coqchk
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/checker/check.ml b/checker/check.ml index 44105aa72f..82341ad9b2 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 |