Bug option -I et -R quand le répertoire est '.'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1035 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 53163a4a1..c128332b2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -84,6 +84,8 @@ let parse_include d =
      Names.dirpath_of_string (String.sub d (pos+1) (String.length d - pos -1)))
   with Not_found ->
     let alias = Filename.basename d in
+    let alias =
+      if alias = "." then Filename.basename (Unix.getcwd ()) else alias in
     if not (Names.is_ident alias) then 
       error ("Cannot find a name to which "^d^" may map in Coq library");
     (d, [alias])