[api] Miscellaneous consolidation + moves to engine.

We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.

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

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))

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

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

library/nameops.ml → 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
+

library/nameops.mli → 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

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)

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 } *)

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 *)

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

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
 

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

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"]

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,15 +616,15 @@ 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 =
   let ldir0 =
     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.")
 

library/library.mllib

@@ -1,5 +1,3 @@
-Univops
-Nameops
 Libnames
 Globnames
 Libobject

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

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
   | _ -> ()

pretyping/pretyping.mllib

@@ -1,3 +1,4 @@
+Geninterp
 Ltac_pretype
 Locusops
 Pretype_errors