From de8888e28ad793511ba2e2969516325b0be44330 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 12 Feb 2015 18:52:09 +0100
Subject: Revert "Using same code for browsing physical directories in coqtop
 and coqdep." (Sorry, was not intended to be pushed)

This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
---
 toplevel/mltop.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'toplevel/mltop.ml')

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index ef2e62c3b..357c5482f 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -11,7 +11,6 @@ open Util
 open Pp
 open Flags
 open Libobject
-open Systemdirs
 open System
 
 (* Code to hook Coq into the ML toplevel -- depends on having the
@@ -156,7 +155,7 @@ let add_ml_dir s =
     | WithoutTop when has_dynlink -> keep_copy_mlpath s
     | _ -> ()
 
-(* For Rec Add ML Path (-R) *)
+(* For Rec Add ML Path *)
 let add_rec_ml_dir unix_path =
   List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path)
 
-- 
cgit v1.2.3