From f42dd8d8530e6227621ccd662741f1da23700304 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:57:08 +0000 Subject: Modulification of dir_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 2 +- library/declare.mli | 2 +- library/declaremods.ml | 32 +++++++++++++------------- library/declaremods.mli | 2 +- library/decls.ml | 4 ++-- library/decls.mli | 6 ++--- library/global.mli | 10 ++++---- library/globnames.ml | 14 ++++++------ library/globnames.mli | 8 +++---- library/lib.ml | 38 +++++++++++++++--------------- library/lib.mli | 26 ++++++++++----------- library/libnames.ml | 61 ++++++++++++++++++++++++------------------------- library/libnames.mli | 52 +++++++++++++++++++++-------------------- library/library.ml | 42 +++++++++++++++++----------------- library/library.mli | 32 +++++++++++++------------- library/nameops.ml | 4 ++-- library/nameops.mli | 4 ++-- library/nametab.ml | 24 +++++++++---------- library/nametab.mli | 20 ++++++++-------- 19 files changed, 192 insertions(+), 191 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index b5670a1a2..015fc9894 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -53,7 +53,7 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types * bool (* Implicit status *) -type variable_declaration = dir_path * section_variable_entry * logical_kind +type variable_declaration = Dir_path.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with diff --git a/library/declare.mli b/library/declare.mli index 09bd6ac8b..54a0160bf 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -32,7 +32,7 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (** opacity *) | SectionLocalAssum of types * bool (** Implicit status *) -type variable_declaration = dir_path * section_variable_entry * logical_kind +type variable_declaration = Dir_path.t * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> object_name diff --git a/library/declaremods.ml b/library/declaremods.ml index b58b355f7..10b04c588 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -123,7 +123,7 @@ let modtab_objects = (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) let openmod_info = - ref ((MPfile(initial_dir),[],None,[]) + ref ((MPfile(Dir_path.initial),[],None,[]) : module_path * mod_bound_id list * (module_struct_entry * int option) option * module_type_body list) @@ -146,16 +146,16 @@ let _ = Summary.declare_summary "MODULE-INFO" Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; - openmod_info := ((MPfile(initial_dir), + openmod_info := ((MPfile(Dir_path.initial), [],None,[])); library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given - by Lib into module_path and dir_path needed for modules *) + by Lib into module_path and Dir_path.t needed for modules *) let mp_of_kn kn = let mp,sec,l = repr_kn kn in - if dir_path_eq sec empty_dirpath then + if Dir_path.equal sec Dir_path.empty then MPdot (mp,l) else anomaly ("Non-empty section in module name!" ^ string_of_kn kn) @@ -246,8 +246,8 @@ let compute_visibility exists what i dir dirinfo = Nametab.Until i (* let do_load_and_subst_module i dir mp substobjs keep = - let prefix = (dir,(mp,empty_dirpath)) in - let dirinfo = DirModule (dir,(mp,empty_dirpath)) in + let prefix = (dir,(mp,Dir_path.empty)) in + let dirinfo = DirModule (dir,(mp,Dir_path.empty)) in let vis = compute_visibility false "load_and_subst" i dir dirinfo in let objects = compute_subst_objects mp substobjs resolver in Nametab.push_dir vis dir dirinfo; @@ -263,8 +263,8 @@ let do_load_and_subst_module i dir mp substobjs keep = *) let do_module exists what iter_objects i dir mp substobjs keep= - let prefix = (dir,(mp,empty_dirpath)) in - let dirinfo = DirModule (dir,(mp,empty_dirpath)) in + let prefix = (dir,(mp,Dir_path.empty)) in + let dirinfo = DirModule (dir,(mp,Dir_path.empty)) in let vis = compute_visibility exists what i dir dirinfo in Nametab.push_dir vis dir dirinfo; modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; @@ -314,7 +314,7 @@ let cache_keep _ = anomaly "This module should not be cached!" let load_keep i ((sp,kn),seg) = let mp = mp_of_kn kn in - let prefix = dir_of_sp sp, (mp,empty_dirpath) in + let prefix = dir_of_sp sp, (mp,Dir_path.empty) in begin try let prefix',objects = MPmap.find mp !modtab_objects in @@ -328,7 +328,7 @@ let load_keep i ((sp,kn),seg) = let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in - open_objects i (dirpath,(mp,empty_dirpath)) seg + open_objects i (dirpath,(mp,Dir_path.empty)) seg let in_modkeep : lib_objects -> obj = declare_object {(default_object "MODULE KEEP OBJECTS") with @@ -506,7 +506,7 @@ let rec get_modtype_substobjs env mp_from inline = function (* add objects associated to them *) let process_module_bindings argids args = let process_arg id (mbid,(mty,ann)) = - let dir = make_dirpath [id] in + let dir = Dir_path.make [id] in let mp = MPbound mbid in let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in @@ -539,7 +539,7 @@ let intern_args interp_modtype (idl,(arg,ann)) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir id) idl in let mty = interp_modtype (Global.env()) arg in - let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in + let dirs = List.map (fun (_,id) -> Dir_path.make [id]) idl in let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env()) (MPbound (List.hd mbids)) inl mty in List.map2 @@ -643,7 +643,7 @@ let module_objects mp = (************************************************************************) (* libraries *) -type library_name = dir_path +type library_name = Dir_path.t (* The first two will form substitutive_objects, the last one is keep *) type library_objects = @@ -885,18 +885,18 @@ let lift_oname (sp,kn) = let cache_include (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in - let prefix = (dir,(mp1,empty_dirpath)) in + let prefix = (dir,(mp1,Dir_path.empty)) in load_objects 1 prefix objs; open_objects 1 prefix objs let load_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in - let prefix = (dir,(mp1,empty_dirpath)) in + let prefix = (dir,(mp1,Dir_path.empty)) in load_objects i prefix objs let open_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in - let prefix = (dir,(mp1,empty_dirpath)) in + let prefix = (dir,(mp1,Dir_path.empty)) in open_objects i prefix objs let subst_include (subst,(me,substobj)) = diff --git a/library/declaremods.mli b/library/declaremods.mli index e52e2620a..650b2cc81 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -104,7 +104,7 @@ val module_objects : module_path -> library_segment (** {6 Libraries i.e. modules on disk } *) -type library_name = dir_path +type library_name = Dir_path.t type library_objects diff --git a/library/decls.ml b/library/decls.ml index 205e51f9b..35b75dab1 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -18,7 +18,7 @@ open Libnames (** Datas associated to section variables and local definitions *) type variable_data = - dir_path * bool (* opacity *) * Univ.constraints * logical_kind + Dir_path.t * bool (* opacity *) * Univ.constraints * logical_kind let vartab = ref (Id.Map.empty : variable_data Id.Map.t) @@ -65,7 +65,7 @@ let initialize_named_context_for_proof () = let last_section_hyps dir = fold_named_context (fun (id,_,_) sec_ids -> - try if dir_path_eq dir (variable_path id) then id::sec_ids else sec_ids + try if Dir_path.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) ~init:[] diff --git a/library/decls.mli b/library/decls.mli index c424eacd3..2e080c7ba 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -18,10 +18,10 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - dir_path * bool (** opacity *) * Univ.constraints * logical_kind + Dir_path.t * bool (** opacity *) * Univ.constraints * logical_kind val add_variable_data : variable -> variable_data -> unit -val variable_path : variable -> dir_path +val variable_path : variable -> Dir_path.t val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind val variable_opacity : variable -> bool @@ -40,4 +40,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val (** Miscellaneous functions *) -val last_section_hyps : dir_path -> Id.t list +val last_section_hyps : Dir_path.t -> Id.t list diff --git a/library/global.mli b/library/global.mli index fdada3f87..dac230a44 100644 --- a/library/global.mli +++ b/library/global.mli @@ -43,9 +43,9 @@ val push_named_def : (Id.t * constr * types option) -> Univ.constraints functions verify that given names match those generated by kernel *) val add_constant : - dir_path -> Id.t -> global_declaration -> constant + Dir_path.t -> Id.t -> global_declaration -> constant val add_mind : - dir_path -> Id.t -> mutual_inductive_entry -> mutual_inductive + Dir_path.t -> Id.t -> mutual_inductive_entry -> mutual_inductive val add_module : Id.t -> module_entry -> inline -> module_path * delta_resolver @@ -59,7 +59,7 @@ val add_constraints : constraints -> unit val set_engagement : engagement -> unit (** {6 Interactive modules and module types } - Both [start_*] functions take the [dir_path] argument to create a + Both [start_*] functions take the [Dir_path.t] argument to create a [mod_self_id]. This should be the name of the compilation unit. *) (** [start_*] functions return the [module_path] valid for components @@ -90,8 +90,8 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive val exists_objlabel : label -> bool (** Compiled modules *) -val start_library : dir_path -> module_path -val export : dir_path -> module_path * compiled_library +val start_library : Dir_path.t -> module_path +val export : Dir_path.t -> module_path * compiled_library val import : compiled_library -> Digest.t -> module_path (** {6 ... } *) diff --git a/library/globnames.ml b/library/globnames.ml index 9ce5451a1..efc46a7ac 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -138,28 +138,28 @@ let constr_of_global_or_constr = function (** {6 Temporary function to brutally form kernel names from section paths } *) -let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id) +let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (label_of_id id) -let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) +let encode_con dir id = make_con (MPfile dir) Dir_path.empty (label_of_id id) let decode_mind kn = let rec dir_of_mp = function - | MPfile dir -> repr_dirpath dir + | MPfile dir -> Dir_path.repr dir | MPbound mbid -> let _,_,dp = repr_mbid mbid in let id = id_of_mbid mbid in - id::(repr_dirpath dp) + id::(Dir_path.repr dp) | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp) in let mp,sec_dir,l = repr_mind kn in - if (repr_dirpath sec_dir) = [] then - (make_dirpath (dir_of_mp mp)),id_of_label l + if (Dir_path.repr sec_dir) = [] then + (Dir_path.make (dir_of_mp mp)),id_of_label l else anomaly "Section part should be empty!" let decode_con kn = let mp,sec_dir,l = repr_con kn in - match mp,(repr_dirpath sec_dir) with + match mp,(Dir_path.repr sec_dir) with MPfile dir,[] -> (dir,id_of_label l) | _ , [] -> anomaly "MPfile expected!" | _ -> anomaly "Section part should be empty!" diff --git a/library/globnames.mli b/library/globnames.mli index b82c68ea7..1e6f143cd 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -80,10 +80,10 @@ val constr_of_global_or_constr : global_reference_or_constr -> constr (** {6 Temporary function to brutally form kernel names from section paths } *) -val encode_mind : dir_path -> Id.t -> mutual_inductive -val decode_mind : mutual_inductive -> dir_path * Id.t -val encode_con : dir_path -> Id.t -> constant -val decode_con : constant -> dir_path * Id.t +val encode_mind : Dir_path.t -> Id.t -> mutual_inductive +val decode_mind : mutual_inductive -> Dir_path.t * Id.t +val encode_con : Dir_path.t -> Id.t -> constant +val decode_con : constant -> Dir_path.t * Id.t (** {6 Popping one level of section in global names } *) diff --git a/library/lib.ml b/library/lib.ml index 6e82bfcb6..ed64b1f40 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -92,7 +92,7 @@ let segment_of_objects prefix = sections, but on the contrary there are many constructions of section paths based on the library path. *) -let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath) +let initial_prefix = default_library,(Names.initial_path,Names.Dir_path.empty) let lib_stk = ref ([] : library_segment) @@ -106,10 +106,10 @@ let library_dp () = let path_prefix = ref initial_prefix let sections_depth () = - List.length (Names.repr_dirpath (snd (snd !path_prefix))) + List.length (Names.Dir_path.repr (snd (snd !path_prefix))) let sections_are_opened () = - match Names.repr_dirpath (snd (snd !path_prefix)) with + match Names.Dir_path.repr (snd (snd !path_prefix)) with [] -> false | _ -> true @@ -127,10 +127,10 @@ let make_path id = Libnames.make_path (cwd ()) id let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id let path_of_include () = - let dir = Names.repr_dirpath (cwd ()) in + let dir = Names.Dir_path.repr (cwd ()) in let new_dir = List.tl dir in let id = List.hd dir in - Libnames.make_path (Names.make_dirpath new_dir) id + Libnames.make_path (Names.Dir_path.make new_dir) id let current_prefix () = snd !path_prefix @@ -275,7 +275,7 @@ let current_mod_id () = let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in - let prefix = dir,(mp,Names.empty_dirpath) in + let prefix = dir,(mp,Names.Dir_path.empty) in let sp = make_path id in let oname = sp, make_kn id in let exists = @@ -328,9 +328,9 @@ let contents_after = function let start_compilation s mp = if !comp_name != None then error "compilation unit is already started"; - if not (Names.dir_path_eq (snd (snd (!path_prefix))) Names.empty_dirpath) then + if not (Names.Dir_path.equal (snd (snd (!path_prefix))) Names.Dir_path.empty) then error "some sections are already opened"; - let prefix = s, (mp, Names.empty_dirpath) in + let prefix = s, (mp, Names.Dir_path.empty) in let _ = add_anonymous_entry (CompilingLibrary prefix) in comp_name := Some s; path_prefix := prefix @@ -356,9 +356,9 @@ let end_compilation dir = match !comp_name with | None -> anomaly "There should be a module name..." | Some m -> - if not (Names.dir_path_eq m dir) then anomaly - ("The current open module has name "^ (Names.string_of_dirpath m) ^ - " and not " ^ (Names.string_of_dirpath m)); + if not (Names.Dir_path.equal m dir) then anomaly + ("The current open module has name "^ (Names.Dir_path.to_string m) ^ + " and not " ^ (Names.Dir_path.to_string m)); in let (after,mark,before) = split_lib_at_opening oname in comp_name := None; @@ -621,7 +621,7 @@ let label_before_name (loc,id) = (* State and initialization. *) -type frozen = Names.dir_path option * library_segment +type frozen = Names.Dir_path.t option * library_segment let freeze () = (!comp_name, !lib_stk) @@ -654,11 +654,11 @@ let rec dp_of_mp modp = let rec split_mp mp = match mp with - | Names.MPfile dp -> dp, Names.empty_dirpath + | Names.MPfile dp -> dp, Names.Dir_path.empty | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in - mprec, Names.make_dirpath (Names.Id.of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [id] + mprec, Names.Dir_path.make (Names.Id.of_string (Names.string_of_label lbl) :: (Names.Dir_path.repr dprec)) + | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.Dir_path.make [id] let split_modpath mp = let rec aux = function @@ -703,13 +703,13 @@ let pop_con con = let con_defined_in_sec kn = let _,dir,_ = Names.repr_con kn in - not (Names.dir_path_eq dir Names.empty_dirpath) && - Names.dir_path_eq (fst (split_dirpath dir)) (snd (current_prefix ())) + not (Names.Dir_path.equal dir Names.Dir_path.empty) && + Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ())) let defined_in_sec kn = let _,dir,_ = Names.repr_mind kn in - not (Names.dir_path_eq dir Names.empty_dirpath) && - Names.dir_path_eq (fst (split_dirpath dir)) (snd (current_prefix ())) + not (Names.Dir_path.equal dir Names.Dir_path.empty) && + Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ())) let discharge_global = function | ConstRef kn when con_defined_in_sec kn -> diff --git a/library/lib.mli b/library/lib.mli index 75e18b194..13a79caf1 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -72,15 +72,15 @@ val contents_after : Libnames.object_name option -> library_segment (** {6 Functions relative to current path } *) (** User-side names *) -val cwd : unit -> Names.dir_path -val cwd_except_section : unit -> Names.dir_path -val current_dirpath : bool -> Names.dir_path (* false = except sections *) +val cwd : unit -> Names.Dir_path.t +val cwd_except_section : unit -> Names.Dir_path.t +val current_dirpath : bool -> Names.Dir_path.t (* false = except sections *) val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path val path_of_include : unit -> Libnames.full_path (** Kernel-side names *) -val current_prefix : unit -> Names.module_path * Names.dir_path +val current_prefix : unit -> Names.module_path * Names.Dir_path.t val make_kn : Names.Id.t -> Names.kernel_name val make_con : Names.Id.t -> Names.constant @@ -124,19 +124,19 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.dir_path -> Names.module_path -> unit -val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment +val start_compilation : Names.Dir_path.t -> Names.module_path -> unit +val end_compilation : Names.Dir_path.t -> Libnames.object_prefix * library_segment -(** The function [library_dp] returns the [dir_path] of the current +(** The function [library_dp] returns the [Dir_path.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.dir_path +val library_dp : unit -> Names.Dir_path.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.module_path -> Names.dir_path -val split_mp : Names.module_path -> Names.dir_path * Names.dir_path -val split_modpath : Names.module_path -> Names.dir_path * Names.Id.t list -val library_part : Globnames.global_reference -> Names.dir_path -val remove_section_part : Globnames.global_reference -> Names.dir_path +val dp_of_mp : Names.module_path -> Names.Dir_path.t +val split_mp : Names.module_path -> Names.Dir_path.t * Names.Dir_path.t +val split_modpath : Names.module_path -> Names.Dir_path.t * Names.Id.t list +val library_part : Globnames.global_reference -> Names.Dir_path.t +val remove_section_part : Globnames.global_reference -> Names.Dir_path.t (** {6 Sections } *) diff --git a/library/libnames.ml b/library/libnames.ml index ee24b2575..8e026d8c2 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,38 +13,38 @@ open Names (**********************************************) -let pr_dirpath sl = (str (string_of_dirpath sl)) +let pr_dirpath sl = (str (Dir_path.to_string sl)) (*s Operations on dirpaths *) (* Pop the last n module idents *) let pop_dirpath_n n dir = - make_dirpath (List.skipn n (repr_dirpath dir)) + Dir_path.make (List.skipn n (Dir_path.repr dir)) -let pop_dirpath p = match repr_dirpath p with +let pop_dirpath p = match Dir_path.repr p with | [] -> anomaly "dirpath_prefix: empty dirpath" - | _::l -> make_dirpath l + | _::l -> Dir_path.make l let is_dirpath_prefix_of d1 d2 = - List.prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + List.prefix_of (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) let chop_dirpath n d = - let d1,d2 = List.chop n (List.rev (repr_dirpath d)) in - make_dirpath (List.rev d1), make_dirpath (List.rev d2) + let d1,d2 = List.chop n (List.rev (Dir_path.repr d)) in + Dir_path.make (List.rev d1), Dir_path.make (List.rev d2) let drop_dirpath_prefix d1 d2 = - let d = Util.List.drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in - make_dirpath (List.rev d) + let d = Util.List.drop_prefix (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) in + Dir_path.make (List.rev d) -let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1) +let append_dirpath d1 d2 = Dir_path.make (Dir_path.repr d2 @ Dir_path.repr d1) (* To know how qualified a name should be to be understood in the current env*) -let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) +let add_dirpath_prefix id d = Dir_path.make (Dir_path.repr d @ [id]) let split_dirpath d = - let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) + let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l) -let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p) +let add_dirpath_suffix p id = Dir_path.make (id :: Dir_path.repr p) (* parsing *) let parse_dir s = @@ -68,23 +68,22 @@ let dirpath_of_string s = | "" -> [] | _ -> parse_dir s in - make_dirpath path + Dir_path.make path -let string_of_dirpath = Names.string_of_dirpath +let string_of_dirpath = Names.Dir_path.to_string - -module Dirset = Set.Make(struct type t = dir_path let compare = dir_path_ord end) -module Dirmap = Map.Make(struct type t = dir_path let compare = dir_path_ord end) +module Dirset = Set.Make(struct type t = Dir_path.t let compare = Dir_path.compare end) +module Dirmap = Map.Make(struct type t = Dir_path.t let compare = Dir_path.compare end) (*s Section paths are absolute names *) type full_path = { - dirpath : dir_path ; + dirpath : Dir_path.t ; basename : Id.t } let eq_full_path p1 p2 = Id.equal p1.basename p2.basename && - Int.equal (dir_path_ord p1.dirpath p2.dirpath) 0 + Int.equal (Dir_path.compare p1.dirpath p2.dirpath) 0 let make_path pa id = { dirpath = pa; basename = id } @@ -93,9 +92,9 @@ let repr_path { dirpath = pa; basename = id } = (pa,id) (* parsing and printing of section paths *) let string_of_path sp = let (sl,id) = repr_path sp in - match repr_dirpath sl with + match Dir_path.repr sl with | [] -> Id.to_string id - | _ -> (string_of_dirpath sl) ^ "." ^ (Id.to_string id) + | _ -> (Dir_path.to_string sl) ^ "." ^ (Id.to_string id) let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 @@ -125,8 +124,8 @@ let pr_path sp = str (string_of_path sp) let restrict_path n sp = let dir, s = repr_path sp in - let dir' = List.firstn n (repr_dirpath dir) in - make_path (make_dirpath dir') s + let dir' = List.firstn n (Dir_path.repr dir) in + make_path (Dir_path.make dir') s (*s qualified names *) type qualid = full_path @@ -142,30 +141,30 @@ let pr_qualid = pr_path let qualid_of_string = path_of_string let qualid_of_path sp = sp -let qualid_of_ident id = make_qualid empty_dirpath id +let qualid_of_ident id = make_qualid Dir_path.empty id let qualid_of_dirpath dir = let (l,a) = split_dirpath dir in make_qualid l a type object_name = full_path * kernel_name -type object_prefix = dir_path * (module_path * dir_path) +type object_prefix = Dir_path.t * (module_path * Dir_path.t) let make_oname (dirpath,(mp,dir)) id = make_path dirpath id, make_kn mp dir (label_of_id id) -(* to this type are mapped dir_path's in the nametab *) +(* to this type are mapped Dir_path.t's in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of dir_path + | DirClosedSection of Dir_path.t (* this won't last long I hope! *) let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = - Int.equal (dir_path_ord d1 d2) 0 && - Int.equal (dir_path_ord p1 p2) 0 && + Int.equal (Dir_path.compare d1 d2) 0 && + Int.equal (Dir_path.compare p1 p2) 0 && mp_eq mp1 mp2 let eq_global_dir_reference r1 r2 = match r1, r2 with @@ -173,7 +172,7 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 | DirModule op1, DirModule op2 -> eq_op op1 op2 -| DirClosedSection dp1, DirClosedSection dp2 -> Int.equal (dir_path_ord dp1 dp2) 0 +| DirClosedSection dp1, DirClosedSection dp2 -> Int.equal (Dir_path.compare dp1 dp2) 0 | _ -> false type reference = diff --git a/library/libnames.mli b/library/libnames.mli index 08330349e..090709549 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -11,31 +11,33 @@ open Loc open Names (** {6 Dirpaths } *) -val pr_dirpath : dir_path -> Pp.std_ppcmds +(** FIXME: ought to be in Names.dir_path *) -val dirpath_of_string : string -> dir_path -val string_of_dirpath : dir_path -> string +val pr_dirpath : Dir_path.t -> Pp.std_ppcmds -(** Pop the suffix of a [dir_path] *) -val pop_dirpath : dir_path -> dir_path +val dirpath_of_string : string -> Dir_path.t +val string_of_dirpath : Dir_path.t -> string + +(** Pop the suffix of a [Dir_path.t] *) +val pop_dirpath : Dir_path.t -> Dir_path.t (** Pop the suffix n times *) -val pop_dirpath_n : int -> dir_path -> dir_path +val pop_dirpath_n : int -> Dir_path.t -> Dir_path.t -(** Give the immediate prefix and basename of a [dir_path] *) -val split_dirpath : dir_path -> dir_path * Id.t +(** Give the immediate prefix and basename of a [Dir_path.t] *) +val split_dirpath : Dir_path.t -> Dir_path.t * Id.t -val add_dirpath_suffix : dir_path -> module_ident -> dir_path -val add_dirpath_prefix : module_ident -> dir_path -> dir_path +val add_dirpath_suffix : Dir_path.t -> module_ident -> Dir_path.t +val add_dirpath_prefix : module_ident -> Dir_path.t -> Dir_path.t -val chop_dirpath : int -> dir_path -> dir_path * dir_path -val append_dirpath : dir_path -> dir_path -> dir_path +val chop_dirpath : int -> Dir_path.t -> Dir_path.t * Dir_path.t +val append_dirpath : Dir_path.t -> Dir_path.t -> Dir_path.t -val drop_dirpath_prefix : dir_path -> dir_path -> dir_path -val is_dirpath_prefix_of : dir_path -> dir_path -> bool +val drop_dirpath_prefix : Dir_path.t -> Dir_path.t -> Dir_path.t +val is_dirpath_prefix_of : Dir_path.t -> Dir_path.t -> bool -module Dirset : Set.S with type elt = dir_path -module Dirmap : Map.S with type key = dir_path +module Dirset : Set.S with type elt = Dir_path.t +module Dirmap : Map.S with type key = Dir_path.t (** {6 Full paths are {e absolute} paths of declarations } *) type full_path @@ -43,11 +45,11 @@ type full_path val eq_full_path : full_path -> full_path -> bool (** Constructors of [full_path] *) -val make_path : dir_path -> Id.t -> full_path +val make_path : Dir_path.t -> Id.t -> full_path (** Destructors of [full_path] *) -val repr_path : full_path -> dir_path * Id.t -val dirpath : full_path -> dir_path +val repr_path : full_path -> Dir_path.t * Id.t +val dirpath : full_path -> Dir_path.t val basename : full_path -> Id.t (** Parsing and printing of section path as ["coq_root.module.id"] *) @@ -67,8 +69,8 @@ val restrict_path : int -> full_path -> full_path type qualid -val make_qualid : dir_path -> Id.t -> qualid -val repr_qualid : qualid -> dir_path * Id.t +val make_qualid : Dir_path.t -> Id.t -> qualid +val repr_qualid : qualid -> Dir_path.t * Id.t val qualid_eq : qualid -> qualid -> bool @@ -80,7 +82,7 @@ val qualid_of_string : string -> qualid qualified name denoting the same name *) val qualid_of_path : full_path -> qualid -val qualid_of_dirpath : dir_path -> qualid +val qualid_of_dirpath : Dir_path.t -> qualid val qualid_of_ident : Id.t -> qualid (** Both names are passed to objects: a "semantic" [kernel_name], which @@ -89,19 +91,19 @@ val qualid_of_ident : Id.t -> qualid type object_name = full_path * kernel_name -type object_prefix = dir_path * (module_path * dir_path) +type object_prefix = Dir_path.t * (module_path * Dir_path.t) val eq_op : object_prefix -> object_prefix -> bool val make_oname : object_prefix -> Id.t -> object_name -(** to this type are mapped [dir_path]'s in the nametab *) +(** to this type are mapped [Dir_path.t]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of dir_path + | DirClosedSection of Dir_path.t (** this won't last long I hope! *) val eq_global_dir_reference : diff --git a/library/library.ml b/library/library.ml index b25b1d313..e2b74c668 100644 --- a/library/library.ml +++ b/library/library.ml @@ -20,7 +20,7 @@ open Lib (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) -type logical_path = dir_path +type logical_path = Dir_path.t let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list) @@ -49,15 +49,15 @@ let add_load_path isroot (phys_path,coq_path) = let filter (p, _, _) = String.equal p phys_path in match List.filter filter !load_paths with | [_,dir,_] -> - if not (dir_path_eq coq_path dir) + if not (Dir_path.equal coq_path dir) (* If this is not the default -I . to coqtop *) && not (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && dir_path_eq coq_path (Nameops.default_root_prefix)) + && Dir_path.equal coq_path (Nameops.default_root_prefix)) then begin (* Assume the user is concerned by library naming *) - if not (dir_path_eq dir Nameops.default_root_prefix) then + if not (Dir_path.equal dir Nameops.default_root_prefix) then Flags.if_warn msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ @@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) = let extend_path_with_dirpath p dir = List.fold_left Filename.concat p - (List.map Id.to_string (List.rev (repr_dirpath dir))) + (List.map Id.to_string (List.rev (Dir_path.repr dir))) let root_paths_matching_dir_path dir = let rec aux = function @@ -90,7 +90,7 @@ let root_paths_matching_dir_path dir = let intersections d1 d2 = let rec aux d1 = - if dir_path_eq d1 empty_dirpath then [d2] else + if Dir_path.equal d1 Dir_path.empty then [d2] else let rest = aux (snd (chop_dirpath 1 d1)) in if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest else rest in @@ -114,7 +114,7 @@ let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) -type compilation_unit_name = dir_path +type compilation_unit_name = Dir_path.t type library_disk = { md_name : compilation_unit_name; @@ -136,8 +136,8 @@ type library_t = { module LibraryOrdered = struct - type t = dir_path - let compare = dir_path_ord + type t = Dir_path.t + let compare = Dir_path.compare end module LibraryMap = Map.Make(LibraryOrdered) @@ -187,7 +187,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (string_of_dirpath dir)) + error ("Unknown library " ^ (Dir_path.to_string dir)) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -210,7 +210,7 @@ let library_is_loaded dir = with Not_found -> false let library_is_opened dir = - List.exists (fun m -> dir_path_eq m.library_name dir) !libraries_imports_list + List.exists (fun m -> Dir_path.equal m.library_name dir) !libraries_imports_list let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list @@ -224,7 +224,7 @@ let opened_libraries () = let register_loaded_library m = let rec aux = function | [] -> [m] - | m'::_ as l when dir_path_eq m'.library_name m.library_name -> l + | m'::_ as l when Dir_path.equal m'.library_name m.library_name -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; libraries_table := LibraryMap.add m.library_name m !libraries_table @@ -238,7 +238,7 @@ let register_loaded_library m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when dir_path_eq m'.library_name m.library_name -> remember_last_of_each l' m + | m'::l' when Dir_path.equal m'.library_name m.library_name -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m let register_open_library export m = @@ -252,7 +252,7 @@ let register_open_library export m = (* [open_library export explicit m] opens library [m] if not already opened _or_ if explicitly asked to be (re)opened *) -let eq_lib_name m1 m2 = dir_path_eq m1.library_name m2.library_name +let eq_lib_name m1 m2 = Dir_path.equal m1.library_name m2.library_name let open_library export explicit_libs m = if @@ -301,7 +301,7 @@ let subst_import (_,o) = o let classify_import (_,export as obj) = if export then Substitute obj else Dispose -let in_import : dir_path * bool -> obj = +let in_import : Dir_path.t * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; @@ -428,7 +428,7 @@ let rec intern_library needed (dir, f) = with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in - if not (dir_path_eq dir m.library_name) then + if not (Dir_path.equal dir m.library_name) then errorlabstrm "load_physical_library" (str ("The file " ^ f ^ " contains library") ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ @@ -441,9 +441,9 @@ and intern_library_deps needed dir m = and intern_mandatory_library caller needed (dir,d) = let m,needed = intern_library needed (try_locate_absolute_library dir) in if not (String.equal d m.library_digest) then - errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^ + errorlabstrm "" (strbrk ("Compiled library "^(Dir_path.to_string caller)^ ".vo makes inconsistent assumptions over library " - ^(string_of_dirpath dir))); + ^(Dir_path.to_string dir))); needed let rec_intern_library needed mref = @@ -525,7 +525,7 @@ let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) -type require_obj = library_t list * dir_path list * bool option +type require_obj = library_t list * Dir_path.t list * bool option let in_require : require_obj -> obj = declare_object {(default_object "REQUIRE") with @@ -596,11 +596,11 @@ let import_module export (loc,qid) = (*s Initializing the compilation of a library. *) let check_coq_overwriting p id = - let l = repr_dirpath p in + let l = Dir_path.repr p in let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (strbrk ("Cannot build module "^string_of_dirpath p^"."^Id.to_string id^ + (strbrk ("Cannot build module "^Dir_path.to_string p^"."^Id.to_string id^ ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) let start_library f = diff --git a/library/library.mli b/library/library.mli index 4e88a85b5..6cf4107cb 100644 --- a/library/library.mli +++ b/library/library.mli @@ -24,7 +24,7 @@ open Libobject (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library : qualid located list -> bool option -> unit -val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit +val require_library_from_dirpath : (Dir_path.t * string) list -> bool option -> unit val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit @@ -34,40 +34,40 @@ val require_library_from_file : val import_module : bool -> qualid located -> unit (** {6 Start the compilation of a library } *) -val start_library : string -> dir_path * string +val start_library : string -> Dir_path.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : dir_path -> string -> unit +val save_library_to : Dir_path.t -> string -> unit (** {6 Interrogate the status of libraries } *) (** - Tell if a library is loaded or opened *) -val library_is_loaded : dir_path -> bool -val library_is_opened : dir_path -> bool +val library_is_loaded : Dir_path.t -> bool +val library_is_opened : Dir_path.t -> bool (** - Tell which libraries are loaded or imported *) -val loaded_libraries : unit -> dir_path list -val opened_libraries : unit -> dir_path list +val loaded_libraries : unit -> Dir_path.t list +val opened_libraries : unit -> Dir_path.t list (** - Return the full filename of a loaded library. *) -val library_full_filename : dir_path -> string +val library_full_filename : Dir_path.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit (** {6 Hook for the xml exportation of libraries } *) -val set_xml_require : (dir_path -> unit) -> unit +val set_xml_require : (Dir_path.t -> unit) -> unit (** {6 ... } *) (** Global load paths: a load path is a physical path in the file - system; to each load path is associated a Coq [dir_path] (the "logical" + system; to each load path is associated a Coq [Dir_path.t] (the "logical" path of the physical path) *) val get_load_paths : unit -> CUnix.physical_path list -val get_full_load_paths : unit -> (CUnix.physical_path * dir_path) list -val add_load_path : bool -> CUnix.physical_path * dir_path -> unit +val get_full_load_paths : unit -> (CUnix.physical_path * Dir_path.t) list +val add_load_path : bool -> CUnix.physical_path * Dir_path.t -> unit val remove_load_path : CUnix.physical_path -> unit -val find_logical_path : CUnix.physical_path -> dir_path +val find_logical_path : CUnix.physical_path -> Dir_path.t val is_in_load_paths : CUnix.physical_path -> bool (** {6 Locate a library in the load paths } *) @@ -76,8 +76,8 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * dir_path * CUnix.physical_path -val try_locate_qualified_library : qualid located -> dir_path * string + bool -> qualid -> library_location * Dir_path.t * CUnix.physical_path +val try_locate_qualified_library : qualid located -> Dir_path.t * string (** {6 Statistics: display the memory use of a library. } *) -val mem : dir_path -> Pp.std_ppcmds +val mem : Dir_path.t -> Pp.std_ppcmds diff --git a/library/nameops.ml b/library/nameops.ml index f8f95135f..361a53d6b 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -138,11 +138,11 @@ let name_fold_map f e = function let pr_lab l = str (string_of_label l) -let default_library = Names.initial_dir (* = ["Top"] *) +let default_library = Names.Dir_path.initial (* = ["Top"] *) (*s Roots of the space of absolute names *) let coq_root = Id.of_string "Coq" -let default_root_prefix = make_dirpath [] +let default_root_prefix = Dir_path.make [] (* Metavariables *) let pr_meta = Pp.int diff --git a/library/nameops.mli b/library/nameops.mli index 3bdd64f75..6e9bde839 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -40,14 +40,14 @@ val pr_lab : label -> Pp.std_ppcmds (** some preset paths *) -val default_library : dir_path +val default_library : Dir_path.t (** This is the root of the standard library of Coq *) val coq_root : module_ident (** This is the default root prefix for developments which doesn't mention a root *) -val default_root_prefix : dir_path +val default_root_prefix : Dir_path.t (** Metavariables *) val pr_meta : Term.metavariable -> Pp.std_ppcmds diff --git a/library/nametab.ml b/library/nametab.ml index bbcee8b66..46d8dcc3f 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -42,7 +42,7 @@ type visibility = Until of int | Exactly of int (* Data structure for nametabs *******************************************) -(* This module type will be instantiated by [full_path] of [dir_path] *) +(* This module type will be instantiated by [full_path] of [Dir_path.t] *) (* The [repr] function is assumed to return the reversed list of idents. *) module type UserName = sig type t @@ -194,7 +194,7 @@ let rec search tree = function let find_node qid tab = let (dir,id) = repr_qualid qid in - search (Id.Map.find id tab) (repr_dirpath dir) + search (Id.Map.find id tab) (Dir_path.repr dir) let locate qid tab = let o = match find_node qid tab with @@ -238,7 +238,7 @@ let shortest_qualid ctx uname tab = in let ptab = Id.Map.find id tab in let found_dir = find_uname [] dir ptab in - make_qualid (make_dirpath found_dir) id + make_qualid (Dir_path.make found_dir) id let push_node node l = match node with @@ -256,7 +256,7 @@ let rec search_prefixes tree = function let find_prefixes qid tab = try let (dir,id) = repr_qualid qid in - search_prefixes (Id.Map.find id tab) (repr_dirpath dir) + search_prefixes (Id.Map.find id tab) (Dir_path.repr dir) with Not_found -> [] end @@ -272,7 +272,7 @@ struct let to_string = string_of_path let repr sp = let dir,id = repr_path sp in - id, (repr_dirpath dir) + id, (Dir_path.repr dir) end module ExtRefEqual = @@ -308,10 +308,10 @@ let the_modtypetab = ref (MPTab.empty : mptab) module DirPath = struct - type t = dir_path - let equal d1 d2 = Int.equal (dir_path_ord d1 d2) 0 - let to_string = string_of_dirpath - let repr dir = match repr_dirpath dir with + type t = Dir_path.t + let equal d1 d2 = Int.equal (Dir_path.compare d1 d2) 0 + let to_string = Dir_path.to_string + let repr dir = match Dir_path.repr dir with | [] -> anomaly "Empty dirpath" | id :: l -> (id, l) end @@ -339,7 +339,7 @@ type globrevtab = full_path Globrevtab.t let the_globrevtab = ref (Globrevtab.empty : globrevtab) -type mprevtab = dir_path MPmap.t +type mprevtab = Dir_path.t MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t @@ -487,7 +487,7 @@ let exists_modtype sp = MPTab.exists sp !the_modtypetab let path_of_global ref = match ref with - | VarRef id -> make_path empty_dirpath id + | VarRef id -> make_path Dir_path.empty id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab let dirpath_of_global ref = @@ -509,7 +509,7 @@ let path_of_tactic kn = let shortest_qualid_of_global ctx ref = match ref with - | VarRef id -> make_qualid empty_dirpath id + | VarRef id -> make_qualid Dir_path.empty id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in ExtRefTab.shortest_qualid ctx sp !the_ccitab diff --git a/library/nametab.mli b/library/nametab.mli index 8a18166a9..188e2dcee 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -17,7 +17,7 @@ open Globnames qualified names (qualid). There are three classes of names: - 1a) internal kernel names: [kernel_name], [constant], [inductive], - [module_path], [dir_path] + [module_path], [Dir_path.t] - 1b) other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... @@ -33,7 +33,7 @@ open Globnames Registers the [object_reference] to be referred to by the [full_user_name] (and its suffixes according to [visibility]). - [full_user_name] can either be a [full_path] or a [dir_path]. + [full_user_name] can either be a [full_path] or a [Dir_path.t]. } {- [exists : full_user_name -> bool] @@ -79,7 +79,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> full_path -> global_reference -> unit val push_modtype : visibility -> full_path -> module_path -> unit -val push_dir : visibility -> dir_path -> global_dir_reference -> unit +val push_dir : visibility -> Dir_path.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit type ltac_constant = kernel_name @@ -98,7 +98,7 @@ val locate_syndef : qualid -> syndef_name val locate_modtype : qualid -> module_path val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path -val locate_section : qualid -> dir_path +val locate_section : qualid -> Dir_path.t val locate_tactic : qualid -> ltac_constant (** These functions globalize user-level references into global @@ -123,15 +123,15 @@ val extended_global_of_path : full_path -> extended_global_reference val exists_cci : full_path -> bool val exists_modtype : full_path -> bool -val exists_dir : dir_path -> bool -val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *) -val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *) +val exists_dir : Dir_path.t -> bool +val exists_section : Dir_path.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_module : Dir_path.t -> bool (** deprecated synonym of [exists_dir] *) (** {6 These functions locate qualids into full user names } *) val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path -val full_name_module : qualid -> dir_path +val full_name_module : qualid -> Dir_path.t (** {6 Reverse lookup } Finding user names corresponding to the given @@ -142,13 +142,13 @@ val full_name_module : qualid -> dir_path val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path -val dirpath_of_module : module_path -> dir_path +val dirpath_of_module : module_path -> Dir_path.t val path_of_tactic : ltac_constant -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) -val dirpath_of_global : global_reference -> dir_path +val dirpath_of_global : global_reference -> Dir_path.t val basename_of_global : global_reference -> Id.t (** Printing of global references using names as short as possible *) -- cgit v1.2.3