[api] Another large deprecation, `Nameops`

5 files changed, 20 insertions, 22 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 109a40a03..0f6452de6 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -171,17 +171,17 @@ let tag_var = tag Tag.variable
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
-    let id = tag_ref (pr_id id) in
+    let id = tag_ref (Id.print id) in
     let sl = match List.rev (DirPath.repr sl) with
     | [] -> mt ()
     | sl ->
-      let pr dir = tag_path (pr_id dir) ++ str "." in
+      let pr dir = tag_path (Id.print dir) ++ str "." in
       prlist pr sl
     in
     sl ++ id
 
-  let pr_id = pr_id
-  let pr_name = pr_name
+  let pr_id = Id.print
+  let pr_name = Name.print
   let pr_qualid = pr_qualid
   let pr_patvar = pr_id
 
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 9ef9162ae..3cc7a3e6b 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -9,7 +9,6 @@
 open Util
 open Pp
 open Genarg
-open Nameops
 open Misctypes
 open Locus
 open Genredexpr
@@ -27,7 +26,7 @@ let pr_located pr (loc, x) =
 
 let pr_or_var pr = function
   | ArgArg x -> pr x
-  | ArgVar (_,s) -> pr_id s
+  | ArgVar (_,s) -> Names.Id.print s
 
 let pr_with_occurrences pr keyword (occs,c) =
   match occs with
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f69c4bce7..acbd2d5d2 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -94,7 +94,7 @@ let print_ref reduce ref =
 (********************************)
 (** Printing implicit arguments *)
 
-let pr_impl_name imp = pr_id (name_of_implicit imp)
+let pr_impl_name imp = Id.print (name_of_implicit imp)
 
 let print_impargs_by_name max = function
   | []  -> []
@@ -238,7 +238,7 @@ let print_primitive_record recflag mipv = function
     | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
     | Decl_kinds.BiFinite -> str " with eta conversion"
     in
-    [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
+    [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
   | _ -> []
 
 let print_primitive ref =
@@ -271,7 +271,7 @@ let print_name_infos ref =
 
 let print_id_args_data test pr id l =
   if List.exists test l then
-    pr (str "For " ++ pr_id id) l
+    pr (str "For " ++ Id.print id) l
   else
     []
 
@@ -456,7 +456,7 @@ let print_located_qualid name flags ref =
     | [] ->
 	let (dir,id) = repr_qualid qid in
 	if DirPath.is_empty dir then
-	  str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id
+	  str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id
 	else
 	  str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid
     | l ->
@@ -608,7 +608,7 @@ let gallina_print_syntactic_def kn =
   hov 2
     (hov 4
        (str "Notation " ++ pr_qualid qid ++
-        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
+        prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++
         spc () ++ str ":=") ++
      spc () ++
      Constrextern.without_specific_symbols
@@ -638,7 +638,7 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
       | (_,s) -> None
 
 let gallina_print_library_entry with_values ent =
-  let pr_name (sp,_) = pr_id (basename sp) in
+  let pr_name (sp,_) = Id.print (basename sp) in
   match ent with
     | (oname,Lib.Leaf lobj) ->
 	gallina_print_leaf_entry with_values (oname,lobj)
diff --git a/printing/printer.ml b/printing/printer.ml
index 751e91cf0..075b03b7d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -478,7 +478,7 @@ let pr_predicate pr_elt (b, elts) =
       if List.is_empty elts then str"none" else pr_elts
 
 let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
-let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p)
+let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p)
 
 let pr_transparent_state (ids, csts) =
   hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 6b3b177aa..0abca0160 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -12,7 +12,6 @@ open Pp
 open Names
 open Environ
 open Declarations
-open Nameops
 open Globnames
 open Libnames
 open Goptions
@@ -80,7 +79,7 @@ let print_params env sigma params =
 let print_constructors envpar sigma names types =
   let pc =
     prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
+      (fun (id,c) -> Id.print id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
       (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
   in
   hv 0 (str "  " ++ pc)
@@ -107,7 +106,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     else mt ()
   in
   hov 0 (
-    pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
+    Id.print mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
     str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
 
@@ -189,15 +188,15 @@ let print_record env mind mib =
       Printer.pr_cumulative
         (Declareops.inductive_is_polymorphic mib)
         (Declareops.inductive_is_cumulative mib) ++
-      def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
+      def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++
       print_params env sigma params ++
       str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
-      str ":= " ++ pr_id mip.mind_consnames.(0)) ++
+      str ":= " ++ Id.print mip.mind_consnames.(0)) ++
     brk(1,2) ++
     hv 2 (str "{ " ++
       prlist_with_sep (fun () -> str ";" ++ brk(2,0))
         (fun (id,b,c) ->
-          pr_id id ++ str (if b then " : " else " := ") ++
+          Id.print id ++ str (if b then " : " else " := ") ++
           Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
     match mib.mind_universes with
     | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
@@ -215,9 +214,9 @@ let pr_mutual_inductive_body env mind mib =
 (** Modpaths *)
 
 let rec print_local_modpath locals = function
-  | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals)
+  | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals)
   | MPdot(mp,l) ->
-      print_local_modpath locals mp ++ str "." ++ pr_lab l
+      print_local_modpath locals mp ++ str "." ++ Label.print l
   | MPfile _ -> raise Not_found
 
 let print_modpath locals mp =
@@ -403,7 +402,7 @@ let rec print_functor fty fatom is_type env mp locals = function
       let kwd = if is_type then "Funsig" else "Functor" in
       hov 2
         (keyword kwd ++ spc () ++
-	 str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++
+	 str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++
 	 spc() ++ print_functor fty fatom is_type env' mp locals' me2)
 
 let rec print_expression x =