[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.

12 files changed, 49 insertions, 436 deletions

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/library/nameops.ml b/library/nameops.ml
deleted file mode 100644
index d598a63b8..000000000
--- a/library/nameops.ml
+++ /dev/null
@@ -1,215 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Util
-open Names
-
-(* Identifiers *)
-
-let pr_id id = Id.print id
-
-(* Utilities *)
-
-let code_of_0 = Char.code '0'
-let code_of_9 = Char.code '9'
-
-let cut_ident skip_quote s =
-  let s = Id.to_string s in
-  let slen = String.length s in
-  (* [n'] is the position of the first non nullary digit *)
-  let rec numpart n n' =
-    if Int.equal n 0 then
-      (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
-      slen
-    else
-      let c = Char.code (String.get s (n-1)) in
-      if Int.equal c code_of_0 && not (Int.equal n slen) then
-	numpart (n-1) n'
-      else if code_of_0 <= c && c <= code_of_9 then
-	numpart (n-1) (n-1)
-      else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then
-	numpart (n-1) (n-1)
-      else
-	n'
-  in
-  numpart slen slen
-
-let repr_ident s =
-  let numstart = cut_ident false s in
-  let s = Id.to_string s in
-  let slen = String.length s in
-  if Int.equal numstart slen then
-    (s, None)
-  else
-    (String.sub s 0 numstart,
-     Some (int_of_string (String.sub s numstart (slen - numstart))))
-
-let make_ident sa = function
-  | Some n ->
-      let c = Char.code (String.get sa (String.length sa -1)) in
-      let s =
-        if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n)
-        else sa ^ "_" ^ (string_of_int n) in
-      Id.of_string s
-  | None -> Id.of_string sa
-
-let root_of_id id =
-  let suffixstart = cut_ident true id in
-  Id.of_string (String.sub (Id.to_string id) 0 suffixstart)
-
-(* Return the same identifier as the original one but whose {i subscript} is incremented.
-   If the original identifier does not have a suffix, [0] is appended to it.
-
-   Example mappings:
-
-   [bar]   ↦ [bar0]
-   [bar0]  ↦ [bar1]
-   [bar00] ↦ [bar01]
-   [bar1]  ↦ [bar2]
-   [bar01] ↦ [bar01]
-   [bar9]  ↦ [bar10]
-   [bar09] ↦ [bar10]
-   [bar99] ↦ [bar100]
-*)
-let increment_subscript id =
-  let id = Id.to_string id in
-  let len = String.length id in
-  let rec add carrypos =
-    let c = id.[carrypos] in
-    if is_digit c then
-      if Int.equal (Char.code c) (Char.code '9') then begin
-	assert (carrypos>0);
-	add (carrypos-1)
-      end
-      else begin
-	let newid = Bytes.of_string id in
-	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
-	Bytes.set newid carrypos (Char.chr (Char.code c + 1));
-	newid
-      end
-    else begin
-      let newid = Bytes.of_string (id^"0") in
-      if carrypos < len-1 then begin
-	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
-	Bytes.set newid (carrypos+1) '1'
-      end;
-      newid
-    end
-  in Id.of_bytes (add (len-1))
-
-let has_subscript id =
-  let id = Id.to_string id in
-  is_digit (id.[String.length id - 1])
-
-let forget_subscript id =
-  let numstart = cut_ident false id in
-  let newid = Bytes.make (numstart+1) '0' in
-  String.blit (Id.to_string id) 0 newid 0 numstart;
-  (Id.of_bytes newid)
-
-let add_suffix id s = Id.of_string (Id.to_string id ^ s)
-let add_prefix s id = Id.of_string (s ^ Id.to_string id)
-
-let atompart_of_id id = fst (repr_ident id)
-
-(* Names *)
-
-module type ExtName =
-sig
-
-  include module type of struct include Names.Name end
-
-  exception IsAnonymous
-
-  val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a
-  val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
-  val iter : (Id.t -> unit) -> t -> unit
-  val map : (Id.t -> Id.t) -> t -> t
-  val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
-  val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
-  val get_id : t -> Id.t
-  val pick : t -> t -> t
-  val cons : t -> Id.t list -> Id.t list
-  val to_option : Name.t -> Id.t option
-
-end
-
-module Name : ExtName =
-struct
-
-  include Names.Name
-
-  exception IsAnonymous
-
-  let fold_left f a = function
-    | Name id -> f a id
-    | Anonymous -> a
-
-  let fold_right f na a =
-    match na with
-    | Name id -> f id a
-    | Anonymous -> a
-
-  let iter f na = fold_right (fun x () -> f x) na ()
-
-  let map f = function
-    | Name id -> Name (f id)
-    | Anonymous -> Anonymous
-
-  let fold_left_map f a = function
-    | Name id -> let (a, id) = f a id in (a, Name id)
-    | Anonymous -> a, Anonymous
-
-  let fold_right_map f na a = match na with
-    | Name id -> let (id, a) = f id a in (Name id, a)
-    | Anonymous -> Anonymous, a
-
-  let get_id = function
-    | Name id -> id
-    | Anonymous -> raise IsAnonymous
-
-  let pick na1 na2 =
-    match na1 with
-    | Name _ -> na1
-    | Anonymous -> na2
-
-  let cons na l =
-    match na with
-    | Anonymous -> l
-    | Name id -> id::l
-
-  let to_option = function
-    | Anonymous -> None
-    | Name id -> Some id
-
-end
-
-open Name
-
-(* Compatibility *)
-let out_name = get_id
-let name_fold = fold_right
-let name_iter = iter
-let name_app = map
-let name_fold_map = fold_left_map
-let name_cons = cons
-let name_max = pick
-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
diff --git a/library/nameops.mli b/library/nameops.mli
deleted file mode 100644
index 60e5a90bb..000000000
--- a/library/nameops.mli
+++ /dev/null
@@ -1,136 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-
-(** Identifiers and names *)
-
-val make_ident : string -> int option -> Id.t
-val repr_ident : Id.t -> string * int option
-
-val atompart_of_id : Id.t -> string  (** remove trailing digits *)
-val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
-
-val add_suffix : Id.t -> string -> Id.t
-val add_prefix : string -> Id.t -> Id.t
-
-(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *)
-
-val has_subscript       : Id.t -> bool
-
-val increment_subscript : Id.t -> Id.t
-(** Return the same identifier as the original one but whose {i subscript} is incremented.
-    If the original identifier does not have a suffix, [0] is appended to it.
-
-    Example mappings:
-
-    [bar]   ↦ [bar0]
-
-    [bar0]  ↦ [bar1]
-
-    [bar00] ↦ [bar01]
-
-    [bar1]  ↦ [bar2]
-
-    [bar01] ↦ [bar01]
-
-    [bar9]  ↦ [bar10]
-
-    [bar09] ↦ [bar10]
-
-    [bar99] ↦ [bar100]
-*)
-
-val forget_subscript    : Id.t -> Id.t
-
-module Name : sig
-
-  include module type of struct include Names.Name end
-
-  exception IsAnonymous
-
-  val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a
-  (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *)
-
-  val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-  (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *)
-
-  val iter : (Id.t -> unit) -> Name.t -> unit
-  (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *)
-
-  val map : (Id.t -> Id.t) -> Name.t -> t
-  (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)
-
-  val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-  (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
-      It is [a,Anonymous] otherwise. *)
-
-  val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
-  (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')].
-      It is [Anonymous,a] otherwise. *)
-
-  val get_id : Name.t -> Id.t
-  (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
-
-  val pick : Name.t -> Name.t -> Name.t
-  (** [pick na na'] returns [Anonymous] if both names are [Anonymous].
-      Pick one of [na] or [na'] otherwise. *)
-
-  val cons : Name.t -> Id.t list -> Id.t list
-  (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
-
-  val to_option : Name.t -> Id.t option
-  (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *)
-
-end
-
-val out_name : Name.t -> Id.t
-[@@ocaml.deprecated "Same as [Name.get_id]"]
-
-val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-[@@ocaml.deprecated "Same as [Name.fold_right]"]
-
-val name_iter : (Id.t -> unit) -> Name.t -> unit
-[@@ocaml.deprecated "Same as [Name.iter]"]
-
-val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.map]"]
-
-val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-[@@ocaml.deprecated "Same as [Name.fold_left_map]"]
-
-val name_max : Name.t -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.pick]"]
-
-val name_cons : Name.t -> Id.t list -> Id.t list
-[@@ocaml.deprecated "Same as [Name.cons]"]
-
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "Same as [Name.print]"]
-
-val pr_id : Id.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Id.print]"]
-
-val pr_lab : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Label.print]"]
-
-(** 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
-
-(** Metavariables *)
-val pr_meta : Constr.metavariable -> Pp.t
-val string_of_meta : Constr.metavariable -> string
diff --git a/library/univops.ml b/library/univops.ml
deleted file mode 100644
index 9dc138eb8..000000000
--- a/library/univops.ml
+++ /dev/null
@@ -1,40 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Constr
-open Univ
-
-let universes_of_constr c =
-  let rec aux s c = 
-    match kind c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) -> 
-      let u = Term.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
-
-let restrict_universe_context (univs,csts) s =
-  (* Universes that are not necessary to typecheck the term.
-     E.g. univs introduced by tactics and not used in the proof term. *)
-  let diff = LSet.diff univs s in
-  let rec aux diff candid univs ness = 
-    let (diff', candid', univs', ness') = 
-      Constraint.fold
-	(fun (l, d, r as c) (diff, candid, univs, csts) ->
-	  if not (LSet.mem l diff) then
-	    (LSet.remove r diff, candid, univs, Constraint.add c csts)
-	  else if not (LSet.mem r diff) then
-	    (LSet.remove l diff, candid, univs, Constraint.add c csts)
-	  else (diff, Constraint.add c candid, univs, csts))
-	candid (diff, Constraint.empty, univs, ness)
-    in
-      if ness' == ness then (LSet.diff univs diff', ness)
-      else aux diff' candid' univs' ness'
-  in aux diff csts univs Constraint.empty
diff --git a/library/univops.mli b/library/univops.mli
deleted file mode 100644
index 9af568bcb..000000000
--- a/library/univops.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Constr
-open Univ
-
-(** Shrink a universe context to a restricted set of variables *)
-
-val universes_of_constr : constr -> LSet.t
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t