Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de DischargeAt)

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

4 files changed, 7 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 84cc2e5751..2383ca304f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -17,12 +17,12 @@ open Impargs
 open Indrec
 
 type strength = 
-  | DischargeAt of section_path 
+  | DischargeAt of dir_path
   | NeverDischarge
 
 let make_strength = function
   | [] -> NeverDischarge
-  | l  -> DischargeAt (sp_of_wd l)
+  | l  -> DischargeAt l
 
 let make_strength_0 () = make_strength (Lib.cwd())
 
diff --git a/library/declare.mli b/library/declare.mli
index b8e45bdea6..6dfcb40650 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -17,7 +17,7 @@ open Inductive
    [Nametab] and [Impargs]. *)
 
 type strength = 
-  | DischargeAt of section_path 
+  | DischargeAt of dir_path
   | NeverDischarge
 
 type section_variable_entry =
diff --git a/library/lib.ml b/library/lib.ml
index 171714c0ec..74986d6fe2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -28,7 +28,7 @@ and library_segment = library_entry list
 let lib_stk = ref ([] : (section_path * node) list)
 
 let module_name = ref None
-let path_prefix = ref ([] : string list)
+let path_prefix = ref ([] : dir_path)
 
 let recalc_path_prefix () =
   let rec recalc = function
@@ -189,7 +189,7 @@ let reset_name id =
   with Not_found ->
     error (string_of_id id ^ ": no such entry")
 
-let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
+let is_section_p sp = dirpath_prefix_of sp !path_prefix
 
 (* State and initialization. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index cf8b173b0f..c6a0ba6803 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -43,8 +43,8 @@ val open_section : string -> section_path
 val close_section : string -> section_path * library_segment
 
 val make_path : identifier -> path_kind -> section_path
-val cwd : unit -> string list
-val is_section_p : section_path -> bool
+val cwd : unit -> dir_path
+val is_section_p : dir_path -> bool
 
 val start_module : string -> unit
 val export_module : unit -> library_segment