From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 2 Jan 2016 17:11:03 +0100
Subject: Remove some unused functions.

Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
---
 library/loadpath.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'library/loadpath.ml')

diff --git a/library/loadpath.ml b/library/loadpath.ml
index 16b419454..f77bd1ef5 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit =
       end
   | _ -> anomaly_too_many_paths phys_path
 
-let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p
-    (List.rev_map Id.to_string (DirPath.repr dir))
-
 let filter_path f =
   let rec aux = function
   | [] -> []
-- 
cgit v1.2.3