Lissage de la gestion des chemins de chargement de fichiers :

- Option -R fait maintenant des Import à tous les niveaux de la
  hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche.
- Option -I rend maintenant possible l'accès aux sous-répertoires via
  les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il
  rend récursivement visibles les noms non qualifiés.
- Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir.
- Ajout option -exclude-dir pour exclure certains sous-répertoires de
  la descente récursive de -R.
- Amélioration message de localisation pour fichiers venant d'un "state".
- Adaptation du checker (et ajout du test check_coq_overwriting qui
  semblait involontairement oublié dans l'option -R).


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

1 files changed, 2 insertions, 2 deletions

diff --git a/checker/check.ml b/checker/check.ml
index f8844975a..bc36f2732 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -209,7 +209,7 @@ let locate_absolute_library dir =
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = string_of_id base^".vo" in
-    let _, file = System.where_in_path loadpath name in
+    let _, file = System.where_in_path false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -229,7 +229,7 @@ let locate_qualified_library qid =
     in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  qid.basename^".vo" in
-    let path, file = System.where_in_path loadpath name in
+    let path, file = System.where_in_path true loadpath name in
     let dir =
       extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
     (* Look if loaded *)