Merge PR #6186: [api] Miscellaneous consolidation.

4 files changed, 16 insertions, 15 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index fd0027c408..257c003b5a 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -8,8 +8,8 @@
 
 open Pp
 open CErrors
+open Sorts
 open Util
-open Term
 open Constr
 open Vars
 open Termops
@@ -376,8 +376,8 @@ let rec check_anonymous_type ind =
     | _ -> false
 
 let make_conclusion_flexible evdref ty poly =
-  if poly && isArity ty then
-    let _, concl = destArity ty in
+  if poly && Term.isArity ty then
+    let _, concl = Term.destArity ty in
       match concl with
       | Type u -> 
         (match Univ.universe_level u with
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 839064aa06..e8c5aeedd1 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -11,7 +11,7 @@ open Util
 open Names
 open Nameops
 open Namegen
-open Term
+open Constr
 open Termops
 open Indtypes
 open Environ
@@ -405,7 +405,7 @@ let explain_not_product env sigma c =
   let pr = pr_lconstr_env env sigma c in
   str "The type of this term is a product" ++ spc () ++
   str "while it is expected to be" ++
-  (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+  (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1bd47a5562..f09b570489 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -8,11 +8,12 @@
 
 open Pp
 open CErrors
+open Term
+open Sorts
 open Util
 open Names
 open Globnames
 open Nameops
-open Term
 open Constr
 open Vars
 open Environ
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 10c139e5ab..6191f37080 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 =