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, 5 insertions, 3 deletions

diff --git a/library/library.mli b/library/library.mli
index 1e2197409..d7cef3243 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -52,6 +52,9 @@ val opened_libraries : unit -> dir_path list
   (* - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
+  (* - Overwrite the filename of all libraries (used when restoring a state) *)
+val overwrite_library_filenames : string -> unit
+
 (*s Hook for the xml exportation of libraries *)
 val set_xml_require : (dir_path -> unit) -> unit
 
@@ -61,11 +64,10 @@ val set_xml_require : (dir_path -> unit) -> unit
 
 val get_load_paths : unit -> System.physical_path list
 val get_full_load_paths : unit -> (System.physical_path * dir_path) list
-val add_load_path : System.physical_path * dir_path -> unit
+val add_load_path : bool -> System.physical_path * dir_path -> unit
 val remove_load_path : System.physical_path -> unit
 val find_logical_path : System.physical_path -> dir_path
 val is_in_load_paths : System.physical_path -> bool
-val load_paths_of_dir_path : dir_path -> System.physical_path list
 
 (*s Locate a library in the load paths *)
 exception LibUnmappedDir
@@ -73,7 +75,7 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  qualid -> library_location * dir_path * System.physical_path
+  bool -> qualid -> library_location * dir_path * System.physical_path
 
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds