From 43a0a3147073b12b038c55c27fd6f0adcb900ac9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 Mar 2015 19:24:10 +0200 Subject: Removing the unused root flag from loadpaths. --- library/loadpath.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'library/loadpath.ml') diff --git a/library/loadpath.ml b/library/loadpath.ml index 0f7c2fb46..ca2280102 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -17,7 +17,6 @@ open Libnames type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_root : bool; path_implicit : bool; } @@ -53,13 +52,12 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path coq_path ~root ~implicit = +let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in let binding = { path_logical = coq_path; path_physical = phys_path; - path_root = root; path_implicit = implicit; } in match List.filter filter !load_paths with -- cgit v1.2.3