From 736ffcea3a04da40ea3047216864ca420f220fe5 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 19 Sep 2013 14:47:23 +0000
Subject: Made the filename of compiled files explicit, i.e. add a ./ prefix
 whenever the filename was given alone. This caused strange behaviour of
 coqtop that was compiling stuff we didn't want to just because it was
 somewhere in its loadpath.

This is why FingerTree was not compiling, btw, as it had two files
equally named in two different paths.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16788 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/coqtop.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 79467cacd4..ed5e92867d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -120,6 +120,13 @@ let add_compile verbose s =
   set_batch_mode ();
   Flags.make_silent true;
   if not !glob_opt then Dumpglob.dump_to_dotglob ();
+  (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
+  let s =
+    let open Filename in
+    if is_implicit s
+    then concat current_dir_name s
+    else s
+  in
   compile_list := (verbose,s) :: !compile_list
 
 let compile_file (v,f) =
-- 
cgit v1.2.3