aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli3
-rw-r--r--dev/top_printers.ml2
-rw-r--r--engine/engine.mllib7
-rw-r--r--engine/evarutil.ml4
-rw-r--r--engine/nameops.ml (renamed from library/nameops.ml)15
-rw-r--r--engine/nameops.mli (renamed from library/nameops.mli)18
-rw-r--r--engine/univops.ml (renamed from library/univops.ml)0
-rw-r--r--engine/univops.mli (renamed from library/univops.mli)0
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/names.mli1
-rw-r--r--library/coqlib.ml10
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/lib.ml6
-rw-r--r--library/libnames.ml10
-rw-r--r--library/libnames.mli20
-rw-r--r--library/library.ml21
-rw-r--r--library/library.mllib2
-rw-r--r--library/loadpath.ml6
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--pretyping/geninterp.ml (renamed from engine/geninterp.ml)0
-rw-r--r--pretyping/geninterp.mli (renamed from engine/geninterp.mli)0
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--printing/ppvernac.ml6
-rw-r--r--printing/prettyp.ml4
-rw-r--r--toplevel/coqinit.ml6
-rw-r--r--vernac/vernacentries.ml18
26 files changed, 99 insertions, 69 deletions
diff --git a/API/API.mli b/API/API.mli
index 86c6f1415..991dca748 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -87,6 +87,7 @@ sig
val repr : t -> Id.t list
val equal : t -> t -> bool
val to_string : t -> string
+ val print : t -> Pp.t
end
module MBId : sig
@@ -1934,8 +1935,10 @@ sig
val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
val dirpath_of_string : string -> Names.DirPath.t
val pr_dirpath : Names.DirPath.t -> Pp.t
+ [@@ocaml.deprecated "Alias for DirPath.print"]
val string_of_path : full_path -> string
+
val basename : full_path -> Names.Id.t
type object_name = full_path * Names.KerName.t
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0f496d3b9..df5f05469 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -39,7 +39,7 @@ let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
let ppid id = pp (Id.print id)
let pplab l = pp (Label.print l)
let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
-let ppdir dir = pp (pr_dirpath dir)
+let ppdir dir = pp (DirPath.print dir)
let ppmp mp = pp(str (ModPath.debug_to_string mp))
let ppcon con = pp(Constant.debug_print con)
let ppproj con = pp(Constant.debug_print (Projection.constant con))
diff --git a/engine/engine.mllib b/engine/engine.mllib
index afc02d7f6..a3614f6c4 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,12 +1,13 @@
-Logic_monad
Universes
+Univops
UState
+Nameops
Evd
EConstr
Namegen
Termops
-Proofview_monad
Evarutil
+Logic_monad
+Proofview_monad
Proofview
Ftactic
-Geninterp
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index df4ef2ce7..14d07ccae 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -11,11 +11,11 @@ open Util
open Names
open Term
open Constr
-open Termops
-open Namegen
open Pre_env
open Environ
open Evd
+open Termops
+open Namegen
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
diff --git a/library/nameops.ml b/engine/nameops.ml
index d598a63b8..5105d7bec 100644
--- a/library/nameops.ml
+++ b/engine/nameops.ml
@@ -203,13 +203,14 @@ let pr_name = print
let pr_lab l = Label.print l
-let default_library = Names.DirPath.initial (* = ["Top"] *)
-
-(*s Roots of the space of absolute names *)
-let coq_string = "Coq"
-let coq_root = Id.of_string coq_string
-let default_root_prefix = DirPath.empty
-
(* Metavariables *)
let pr_meta = Pp.int
let string_of_meta = string_of_int
+
+(* Deprecated *)
+open Libnames
+let default_library = default_library
+let coq_string = coq_string
+let coq_root = coq_root
+let default_root_prefix = default_root_prefix
+
diff --git a/library/nameops.mli b/engine/nameops.mli
index 60e5a90bb..0fec8a925 100644
--- a/library/nameops.mli
+++ b/engine/nameops.mli
@@ -89,6 +89,10 @@ module Name : sig
end
+(** Metavariables *)
+val pr_meta : Constr.metavariable -> Pp.t
+val string_of_meta : Constr.metavariable -> string
+
val out_name : Name.t -> Id.t
[@@ocaml.deprecated "Same as [Name.get_id]"]
@@ -119,18 +123,16 @@ val pr_id : Id.t -> Pp.t
val pr_lab : Label.t -> Pp.t
[@@ocaml.deprecated "Same as [Names.Label.print]"]
-(** some preset paths *)
-
+(** Deprecated stuff to libnames *)
val default_library : DirPath.t
+[@@ocaml.deprecated "Same as [Libnames.default_library]"]
-(** This is the root of the standard library of Coq *)
val coq_root : module_ident (** "Coq" *)
+[@@ocaml.deprecated "Same as [Libnames.coq_root]"]
+
val coq_string : string (** "Coq" *)
+[@@ocaml.deprecated "Same as [Libnames.coq_string]"]
-(** This is the default root prefix for developments which doesn't
- mention a root *)
val default_root_prefix : DirPath.t
+[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]
-(** Metavariables *)
-val pr_meta : Constr.metavariable -> Pp.t
-val string_of_meta : Constr.metavariable -> string
diff --git a/library/univops.ml b/engine/univops.ml
index 9dc138eb8..9dc138eb8 100644
--- a/library/univops.ml
+++ b/engine/univops.ml
diff --git a/library/univops.mli b/engine/univops.mli
index 9af568bcb..9af568bcb 100644
--- a/library/univops.mli
+++ b/engine/univops.mli
diff --git a/kernel/names.ml b/kernel/names.ml
index cb27104d1..b02c0b840 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -179,6 +179,8 @@ struct
| [] -> "<>"
| sl -> String.concat "." (List.rev_map Id.to_string sl)
+ let print dp = str (to_string dp)
+
let initial = [default_module_name]
module Hdir = Hashcons.Hlist(Id)
diff --git a/kernel/names.mli b/kernel/names.mli
index ba0637c8a..709ebeb7f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -159,6 +159,7 @@ sig
val hcons : t -> t
(** Hashconsing of directory paths. *)
+ val print : t -> Pp.t
end
(** {6 Names of structure elements } *)
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 141fff033..4a2390985 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -14,7 +14,7 @@ open Libnames
open Globnames
open Nametab
-let coq = Nameops.coq_string (* "Coq" *)
+let coq = Libnames.coq_string (* "Coq" *)
(************************************************************************)
(* Generic functions to find Coq objects *)
@@ -32,7 +32,7 @@ let find_reference locstr dir s =
of not found errors here *)
user_err ~hdr:locstr
Pp.(str "cannot find " ++ Libnames.pr_path sp ++
- str "; maybe library " ++ Libnames.pr_dirpath dp ++
+ str "; maybe library " ++ DirPath.print dp ++
str " has to be required first.")
let coq_reference locstr dir s = find_reference locstr (coq::dir) s
@@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s =
| [] ->
anomaly ~label:locstr (str "cannot find " ++ str s ++
str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
- prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
+ prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
| l ->
anomaly ~label:locstr
(str "ambiguous name " ++ str s ++ str " can represent " ++
prlist_with_sep pr_comma
(fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
- prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
+ prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
(* For tactics/commands requiring vernacular libraries *)
@@ -79,7 +79,7 @@ let check_required_library d =
*)
(* or failing ...*)
user_err ~hdr:"Coqlib.check_required_library"
- (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
+ (str "Library " ++ DirPath.print dir ++ str " has to be required first.")
(************************************************************************)
(* Specific Coq objects *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index cda40f49f..db83dafef 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -167,13 +167,13 @@ let consistency_checks exists dir dirinfo =
try Nametab.locate_dir (qualid_of_dirpath dir)
with Not_found ->
user_err ~hdr:"consistency_checks"
- (pr_dirpath dir ++ str " should already exist!")
+ (DirPath.print dir ++ str " should already exist!")
in
assert (eq_global_dir_reference globref dirinfo)
else
if Nametab.exists_dir dir then
user_err ~hdr:"consistency_checks"
- (pr_dirpath dir ++ str " already exists")
+ (DirPath.print dir ++ str " already exists")
let compute_visibility exists i =
if exists then Nametab.Exactly i else Nametab.Until i
diff --git a/library/lib.ml b/library/lib.ml
index 36292d367..6abbf7ef9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -12,7 +12,7 @@ open Util
open Names
open Libnames
open Globnames
-open Nameops
+(* open Nameops *)
open Libobject
open Context.Named.Declaration
@@ -361,8 +361,8 @@ let end_compilation_checks dir =
| None -> anomaly (Pp.str "There should be a module name...")
| Some m ->
if not (Names.DirPath.equal m dir) then anomaly
- (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
- spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str ".");
+ (str "The current open module has name" ++ spc () ++ DirPath.print m ++
+ spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str ".");
in
oname
diff --git a/library/libnames.ml b/library/libnames.ml
index efb1348ab..81878e72f 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -13,7 +13,7 @@ open Names
(**********************************************)
-let pr_dirpath sl = str (DirPath.to_string sl)
+let pr_dirpath sl = DirPath.print sl
(*s Operations on dirpaths *)
@@ -232,6 +232,14 @@ let join_reference ns r =
Qualid (loc, make_qualid
(dirpath_of_string (Names.Id.to_string id1)) id2)
+(* Default paths *)
+let default_library = Names.DirPath.initial (* = ["Top"] *)
+
+(*s Roots of the space of absolute names *)
+let coq_string = "Coq"
+let coq_root = Id.of_string coq_string
+let default_root_prefix = DirPath.empty
+
(* Deprecated synonyms *)
let make_short_qualid = qualid_of_ident
diff --git a/library/libnames.mli b/library/libnames.mli
index ab2585334..ed01163ee 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -11,12 +11,13 @@ open Loc
open Names
(** {6 Dirpaths } *)
-(** FIXME: ought to be in Names.dir_path *)
+val dirpath_of_string : string -> DirPath.t
val pr_dirpath : DirPath.t -> Pp.t
+[@@ocaml.deprecated "Alias for DirPath.print"]
-val dirpath_of_string : string -> DirPath.t
val string_of_dirpath : DirPath.t -> string
+[@@ocaml.deprecated "Alias for DirPath.to_string"]
(** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *)
val pop_dirpath : DirPath.t -> DirPath.t
@@ -127,7 +128,20 @@ val pr_reference : reference -> Pp.t
val loc_of_reference : reference -> Loc.t option
val join_reference : reference -> reference -> reference
-(** Deprecated synonyms *)
+(** some preset paths *)
+val default_library : DirPath.t
+
+(** This is the root of the standard library of Coq *)
+val coq_root : module_ident (** "Coq" *)
+val coq_string : string (** "Coq" *)
+(** This is the default root prefix for developments which doesn't
+ mention a root *)
+val default_root_prefix : DirPath.t
+
+(** Deprecated synonyms *)
val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *)
+[@@ocaml.deprecated "Alias for qualid_of_ident"]
+
val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
+[@@ocaml.deprecated "Alias for qualid_of_sp"]
diff --git a/library/library.ml b/library/library.ml
index 99ef66699..88470d121 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -12,9 +12,8 @@ open Util
open Names
open Libnames
-open Nameops
-open Libobject
open Lib
+open Libobject
(************************************************************************)
(*s Low-level interning/externing of libraries to files *)
@@ -132,7 +131,7 @@ let try_find_library dir =
try find_library dir
with Not_found ->
user_err ~hdr:"Library.find_library"
- (str "Unknown library " ++ pr_dirpath dir)
+ (str "Unknown library " ++ DirPath.print dir)
let register_library_filename dir f =
(* Not synchronized: overwrite the previous binding if one existed *)
@@ -331,7 +330,7 @@ let error_unmapped_dir qid =
let prefix, _ = repr_qualid qid in
user_err ~hdr:"load_absolute_library_from"
(str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
- str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
+ str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ())
let error_lib_not_found qid =
user_err ~hdr:"load_absolute_library_from"
@@ -465,8 +464,8 @@ let rec intern_library (needed, contents) (dir, f) from =
if not (DirPath.equal dir m.library_name) then
user_err ~hdr:"load_physical_library"
(str "The file " ++ str f ++ str " contains library" ++ spc () ++
- pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
- spc() ++ pr_dirpath dir);
+ DirPath.print m.library_name ++ spc () ++ str "and not library" ++
+ spc() ++ DirPath.print dir);
Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
m.library_digests, intern_library_deps (needed, contents) dir m f
@@ -477,9 +476,9 @@ and intern_library_deps libs dir m from =
and intern_mandatory_library caller from libs (dir,d) =
let digest, libs = intern_library libs (dir, None) (Some from) in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- user_err (str "Compiled library " ++ pr_dirpath caller ++
+ user_err (str "Compiled library " ++ DirPath.print caller ++
str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
- over library " ++ pr_dirpath dir);
+ over library " ++ DirPath.print dir);
libs
let rec_intern_library libs (dir, f) =
@@ -617,7 +616,7 @@ let check_coq_overwriting p id =
let is_empty = match l with [] -> true | _ -> false in
if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
user_err
- (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
+ (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
let start_library fo =
@@ -625,7 +624,7 @@ let start_library fo =
try
let lp = Loadpath.find_load_path (Filename.dirname fo) in
Loadpath.logical lp
- with Not_found -> Nameops.default_root_prefix
+ with Not_found -> Libnames.default_root_prefix
in
let file = Filename.chop_extension (Filename.basename fo) in
let id = Id.of_string file in
@@ -665,7 +664,7 @@ let current_reexports () = !libraries_exports_list
let error_recursively_dependent_library dir =
user_err
- (strbrk "Unable to use logical name " ++ pr_dirpath dir ++
+ (strbrk "Unable to use logical name " ++ DirPath.print dir ++
strbrk " to save current library because" ++
strbrk " it already depends on a library of this name.")
diff --git a/library/library.mllib b/library/library.mllib
index d94fc2291..e43bfb5a1 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,5 +1,3 @@
-Univops
-Nameops
Libnames
Globnames
Libobject
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 757e972b1..eb6dae84a 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -54,8 +54,8 @@ let warn_overriding_logical_loadpath =
CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
(fun (phys_path, old_path, coq_path) ->
str phys_path ++ strbrk " was previously bound to " ++
- pr_dirpath old_path ++ strbrk "; it is remapped to " ++
- pr_dirpath coq_path)
+ DirPath.print old_path ++ strbrk "; it is remapped to " ++
+ DirPath.print coq_path)
let add_load_path phys_path coq_path ~implicit =
let phys_path = CUnix.canonical_path_name phys_path in
@@ -75,7 +75,7 @@ let add_load_path phys_path coq_path ~implicit =
else
let () =
(* Do not warn when overriding the default "-I ." path *)
- if not (DirPath.equal old_path Nameops.default_root_prefix) then
+ if not (DirPath.equal old_path Libnames.default_root_prefix) then
warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
in
true in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 995d5fd19..5903733a6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -486,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with
if not (Library.library_is_loaded dp) then begin
match base_mp (Lib.current_mp ()) with
| MPfile dp' when not (DirPath.equal dp dp') ->
- err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
+ err (str "Please load library " ++ DirPath.print dp ++ str " first.")
| _ -> ()
end
| _ -> ()
diff --git a/engine/geninterp.ml b/pretyping/geninterp.ml
index 768ef3cfd..768ef3cfd 100644
--- a/engine/geninterp.ml
+++ b/pretyping/geninterp.ml
diff --git a/engine/geninterp.mli b/pretyping/geninterp.mli
index ae0b26e59..ae0b26e59 100644
--- a/engine/geninterp.mli
+++ b/pretyping/geninterp.mli
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 9904b7354..1da5b4567 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,3 +1,4 @@
+Geninterp
Ltac_pretype
Locusops
Pretype_errors
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 143f9ddcc..e897b1938 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -447,7 +447,7 @@ open Decl_kinds
| PrintGrammar ent ->
keyword "Print Grammar" ++ spc() ++ str ent
| PrintLoadPath dir ->
- keyword "Print LoadPath" ++ pr_opt pr_dirpath dir
+ keyword "Print LoadPath" ++ pr_opt DirPath.print dir
| PrintModules ->
keyword "Print Modules"
| PrintMLLoadPath ->
@@ -518,7 +518,7 @@ open Decl_kinds
in
keyword cmd ++ spc() ++ pr_smart_global qid
| PrintNamespace dp ->
- keyword "Print Namespace" ++ pr_dirpath dp
+ keyword "Print Namespace" ++ DirPath.print dp
| PrintStrategy None ->
keyword "Print Strategies"
| PrintStrategy (Some qid) ->
@@ -964,7 +964,7 @@ open Decl_kinds
keyword "LoadPath" ++ spc() ++ qs s ++
(match d with
| None -> mt()
- | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir))
+ | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
)
| VernacRemoveLoadPath s ->
return (keyword "Remove LoadPath" ++ qs s)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e2d23ce7b..060cf6fc7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -366,7 +366,7 @@ let pr_located_qualid = function
| DirModule (dir,_) -> "Module", dir
| DirClosedSection dir -> "Closed Section", dir
in
- str s ++ spc () ++ pr_dirpath dir
+ str s ++ spc () ++ DirPath.print dir
| ModuleType mp ->
str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
| Other (obj, info) -> info.name obj
@@ -647,7 +647,7 @@ let gallina_print_library_entry env sigma with_values ent =
| (oname,Lib.ClosedSection _) ->
Some (str " >>>>>>> Closed Section " ++ pr_name oname)
| (_,Lib.CompilingLibrary (dir,_)) ->
- Some (str " >>>>>>> Library " ++ pr_dirpath dir)
+ Some (str " >>>>>>> Library " ++ DirPath.print dir)
| (oname,Lib.OpenedModule _) ->
Some (str " >>>>>>> Module " ++ pr_name oname)
| (oname,Lib.ClosedModule _) ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index c80899288..3a195c1df 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -65,7 +65,7 @@ let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml =
let add_userlib_path ~unix_path =
Mltop.add_rec_path Mltop.AddRecML ~unix_path
- ~coq_root:Nameops.default_root_prefix ~implicit:false
+ ~coq_root:Libnames.default_root_prefix ~implicit:false
(* Options -I, -I-as, and -R of the command line *)
let includes = ref []
@@ -80,7 +80,7 @@ let init_load_path ~load_init =
let user_contrib = coqlib/"user-contrib" in
let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
let coqpath = Envars.coqpath in
- let coq_root = Names.DirPath.make [Nameops.coq_root] in
+ let coq_root = Names.DirPath.make [Libnames.coq_root] in
(* NOTE: These directories are searched from last to first *)
(* first, developer specific directory to open *)
if Coq_config.local then
@@ -105,7 +105,7 @@ let init_load_path ~load_init =
List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
(* then current directory (not recursively!) *)
Mltop.add_ml_dir ".";
- Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false;
+ Loadpath.add_load_path "." Libnames.default_root_prefix ~implicit:false;
(* additional loadpath, given with options -Q and -R *)
List.iter
(fun (unix_path, coq_root, implicit) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 10c139e5a..6191f3708 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -152,7 +152,7 @@ let show_match id =
(* "Print" commands *)
let print_path_entry p =
- let dir = pr_dirpath (Loadpath.logical p) in
+ let dir = DirPath.print (Loadpath.logical p) in
let path = str (Loadpath.physical p) in
Pp.hov 2 (dir ++ spc () ++ path)
@@ -175,9 +175,9 @@ let print_modules () =
let loaded_opened = List.intersect DirPath.equal opened loaded
and only_loaded = List.subtract DirPath.equal loaded opened in
str"Loaded and imported library files: " ++
- pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++
+ pr_vertical_list DirPath.print loaded_opened ++ fnl () ++
str"Loaded and not imported library files: " ++
- pr_vertical_list pr_dirpath only_loaded
+ pr_vertical_list DirPath.print only_loaded
let print_module r =
@@ -361,29 +361,29 @@ let locate_file f =
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->
Feedback.msg_info (hov 0
- (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
+ (DirPath.print fulldir ++ strbrk " has been loaded from file " ++
str file))
| Library.LibInPath, fulldir, file ->
Feedback.msg_info (hov 0
- (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
+ (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file))
let err_unmapped_library ?loc ?from qid =
let dir = fst (repr_qualid qid) in
let prefix = match from with
| None -> str "."
| Some from ->
- str " and prefix " ++ pr_dirpath from ++ str "."
+ str " and prefix " ++ DirPath.print from ++ str "."
in
user_err ?loc
~hdr:"locate_library"
(strbrk "Cannot find a physical path bound to logical path matching suffix " ++
- pr_dirpath dir ++ prefix)
+ DirPath.print dir ++ prefix)
let err_notfound_library ?loc ?from qid =
let prefix = match from with
| None -> str "."
| Some from ->
- str " with prefix " ++ pr_dirpath from ++ str "."
+ str " with prefix " ++ DirPath.print from ++ str "."
in
user_err ?loc ~hdr:"locate_library"
(strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
@@ -893,7 +893,7 @@ let expand filename =
let vernac_add_loadpath implicit pdir ldiropt =
let pdir = expand pdir in
- let alias = Option.default Nameops.default_root_prefix ldiropt in
+ let alias = Option.default Libnames.default_root_prefix ldiropt in
Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
let vernac_remove_loadpath path =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 07:02:15 +0000