[api] Another large deprecation, `Nameops`

9 files changed, 18 insertions, 21 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index b7b76c830..3a9179813 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -12,7 +12,6 @@ open CErrors
 open Util
 open Names
 open Globnames
-open Nameops
 open Termops
 open Reductionops
 open Term
@@ -55,7 +54,7 @@ exception PatternMatchingFailure
 let warn_meta_collision =
   CWarnings.create ~name:"meta-collision" ~category:"ltac"
          (fun name ->
-          strbrk "Collision between bound variable " ++ pr_id name ++
+          strbrk "Collision between bound variable " ++ Id.print name ++
             strbrk " and a metavariable of same name.")
 
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 9e7652da6..fd6bfe0a2 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -12,7 +12,6 @@ open CErrors
 open Names
 open Locus
 open EConstr
-open Nameops
 open Termops
 open Pretype_errors
 
@@ -30,7 +29,7 @@ let explain_invalid_occurrence l =
   ++ prlist_with_sep spc int l ++ str "."
 
 let explain_incorrect_in_value_occurrence id =
-  pr_id id ++ str " has no value."
+  Id.print id ++ str " has no value."
 
 let explain_occurrence_error = function
   | InvalidOccurrence l -> explain_invalid_occurrence l
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 055fd68f6..093f1f0b6 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -290,7 +290,7 @@ let warn_variable_collision =
   let open Pp in
   CWarnings.create ~name:"variable-collision" ~category:"ltac"
          (fun name ->
-          strbrk "Collision between bound variables of name " ++ pr_id name)
+          strbrk "Collision between bound variables of name " ++ Id.print name)
 
 let add_and_check_ident id set =
   if Id.Set.mem id set then warn_variable_collision id;
@@ -524,7 +524,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
       try Name (Id.Map.find id ltac_idents)
       with Not_found ->
         if Id.Map.mem id ltac_genargs then
-          user_err (str"Ltac variable"++spc()++ pr_id id ++
+          user_err (str"Ltac variable"++spc()++ Id.print id ++
                            spc()++str"is not bound to an identifier."++spc()++
                            str"It cannot be used in a binder.")
         else n
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 48b33e708..b7b5b1662 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -616,7 +616,7 @@ let lookup_eliminator ind_sp s =
   with Not_found ->
     user_err ~hdr:"default_elim"
       (strbrk "Cannot find the elimination combinator " ++
-       pr_id id ++ strbrk ", the elimination of the inductive definition " ++
+       Id.print id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Id.Set.empty (IndRef ind_sp) ++
        strbrk " on sort " ++ Termops.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ee79b5474..4d8c09c50 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -230,8 +230,8 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  user_err  (str "Cannot substitute the term bound to " ++ pr_id id
-    ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
+  user_err  (str "Cannot substitute the term bound to " ++ Id.print id
+    ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
 let instantiate_pattern env sigma lvar c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b2b583ba7..e3470b0f1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -382,9 +382,9 @@ let check_instance loc subst = function
   | [] -> ()
   | (id,_) :: _ ->
       if List.mem_assoc id subst then
-        user_err ?loc  (pr_id id ++ str "appears more than once.")
+        user_err ?loc  (Id.print id ++ str "appears more than once.")
       else
-        user_err ?loc  (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+        user_err ?loc  (str "No such variable in the signature of the existential variable: " ++ Id.print id ++ str ".")
 
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
@@ -410,8 +410,8 @@ let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
-    user_err  (str "Ltac variable " ++ pr_id id0 ++
-		       str " depends on pattern variable name " ++ pr_id id ++
+    user_err  (str "Ltac variable " ++ Id.print id0 ++
+		       str " depends on pattern variable name " ++ Id.print id ++
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
@@ -454,7 +454,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
       if Id.Map.mem id lvar.ltac_genargs then begin
         let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
 	user_err ?loc 
-         (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
+         (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \
           bound to a " ++ Geninterp.Val.pr typ ++ str ".")
       end;
       (* Check if [id] is a section or goal variable *)
@@ -1089,7 +1089,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
       with Not_found ->
         user_err ?loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
-          str " in current context: no binding for " ++ pr_id id ++ str ".") in
+          str " in current context: no binding for " ++ Id.print id ++ str ".") in
     ((id,c)::subst, update) in
   let subst,inst = List.fold_right f hyps ([],update) in
   check_instance loc subst inst;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cb24ca804..e6d8a0af2 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -300,7 +300,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
 let error_not_structure ref =
   user_err ~hdr:"object_declare"
-    (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
+    (Id.print (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5eb6b780a..a4e2f90d4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1628,7 +1628,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context_val x (named_context_val env) then
       user_err ~hdr:"Unification.make_abstraction_core"
-        (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
+        (str "The variable " ++ Id.print x ++ str " is already declared.")
     else
       x
   in
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index d7c42d03a..5576e33f4 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,10 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Nameops
-open CErrors
 open Pp
+open CErrors
+open Names
 
 (** Local universes and constraints declarations *)
 type universe_decl =
@@ -34,7 +33,7 @@ let interp_univ_constraints env evd cstrs =
     | GType (Some (loc, Name id)) ->
        try loc, Evd.universe_of_name evd (Id.to_string id)
        with Not_found ->
-         user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id)
+         user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id)
   in
   let interp (evd,cstrs) (u, d, u') =
     let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in