[api] Another large deprecation, `Nameops`

8 files changed, 40 insertions, 43 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a0a749bfb..c4e0ac500 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -122,7 +122,7 @@ type internalization_error =
 exception InternalizationError of internalization_error Loc.located
 
 let explain_variable_capture id id' =
-  pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++
+  Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++
   strbrk ": cannot interpret both of them with the same type"
 
 let explain_illegal_metavariable =
@@ -132,12 +132,12 @@ let explain_not_a_constructor ref =
   str "Unknown constructor: " ++ pr_reference ref
 
 let explain_unbound_fix_name is_cofix id =
-  str "The name" ++ spc () ++ pr_id id ++
+  str "The name" ++ spc () ++ Id.print id ++
   spc () ++ str "is not bound in the corresponding" ++ spc () ++
   str (if is_cofix then "co" else "") ++ str "fixpoint definition"
 
 let explain_non_linear_pattern id =
-  str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
+  str "The variable " ++ Id.print id ++ str " is bound several times in pattern"
 
 let explain_bad_patterns_number n1 n2 =
   str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
@@ -163,7 +163,7 @@ let error_parameter_not_implicit ?loc =
     "they must be replaced by '_'.")
 
 let error_ldots_var ?loc =
-  user_err ?loc  (str "Special token " ++ pr_id ldots_var ++
+  user_err ?loc  (str "Special token " ++ Id.print ldots_var ++
     str " is for use in the Notation command.")
 
 (**********************************************************************)
@@ -263,13 +263,13 @@ let pr_scope_stack = function
 
 let error_inconsistent_scope ?loc id scopes1 scopes2 =
   user_err ?loc ~hdr:"set_var_scope"
-   (pr_id id ++ str " is here used in " ++
+   (Id.print id ++ str " is here used in " ++
     pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
     pr_scope_stack scopes1)
 
 let error_expect_binder_notation_type ?loc id =
   user_err ?loc 
-   (pr_id id ++
+   (Id.print id ++
     str " is expected to occur in binding position in the right-hand side.")
 
 let set_var_scope ?loc id istermvar env ntnvars =
@@ -365,7 +365,7 @@ let check_hidden_implicit_parameters ?loc id impls =
     | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams
     | _ -> false) impls
   then
-    user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++
+    user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++
       strbrk "a parameter of the inductive type; bound variables in " ++
       strbrk "the type of a constructor shall use a different name.")
 
@@ -743,7 +743,7 @@ let string_of_ty = function
 let gvar (loc, id) us = match us with
 | None -> DAst.make ?loc @@ GVar id
 | Some _ ->
-  user_err ?loc  (str "Variable " ++ pr_id id ++
+  user_err ?loc  (str "Variable " ++ Id.print id ++
     str " cannot have a universe instance")
 
 let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
@@ -772,7 +772,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err ?loc ~hdr:"intern_var"
-     (str "variable " ++ pr_id id ++ str " should be bound to a term.")
+     (str "variable " ++ Id.print id ++ str " should be bound to a term.")
   else
     (* Is [id] a goal or section variable *)
     let _ = Context.Named.lookup id namedctx in
@@ -1570,9 +1570,9 @@ let extract_explicit_arg imps args =
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
 		user_err ?loc 
-		  (str "Wrong argument name: " ++ pr_id id ++ str ".");
+		  (str "Wrong argument name: " ++ Id.print id ++ str ".");
 	      if Id.Map.mem id eargs then
-		user_err ?loc  (str "Argument name " ++ pr_id id
+		user_err ?loc  (str "Argument name " ++ Id.print id
 		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
@@ -1990,7 +1990,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	    (let (id,(loc,_)) = Id.Map.choose eargs in
 	       user_err ?loc  (str "Not enough non implicit \
 	    arguments to accept the argument bound to " ++
-		 pr_id id ++ str"."));
+		 Id.print id ++ str"."));
 	  []
       | ([], rargs) ->
 	  assert (Id.Map.is_empty eargs);
diff --git a/interp/declare.ml b/interp/declare.ml
index 0cc4d0fca..1a589897b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -14,7 +14,6 @@ open Util
 open Names
 open Libnames
 open Globnames
-open Nameops
 open Constr
 open Declarations
 open Entries
@@ -46,7 +45,7 @@ let cache_variable ((sp,_),o) =
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
-    alreadydeclared (pr_id id ++ str " already exists");
+    alreadydeclared (Id.print id ++ str " already exists");
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
@@ -107,7 +106,7 @@ type constant_declaration = Safe_typing.private_constants constant_entry * logic
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn), obj) =
   if Nametab.exists_cci sp then
-    alreadydeclared (pr_id (basename sp) ++ str " already exists");
+    alreadydeclared (Id.print (basename sp) ++ str " already exists");
   let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
   add_constant_kind con obj.cst_kind
@@ -132,7 +131,7 @@ let exists_name id =
 
 let check_exists sp =
   let id = basename sp in
-  if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+  if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
 
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
@@ -407,11 +406,11 @@ let pr_rank i = pr_nth (i+1)
 let fixpoint_message indexes l =
   Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "no recursive definition.")
-  | [id] -> pr_id id ++ str " is recursively defined" ++
+  | [id] -> Id.print id ++ str " is recursively defined" ++
       (match indexes with
 	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
 	 | _ -> mt ())
-  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
 		  spc () ++ str "are recursively defined" ++
 		  match indexes with
 		    | Some a -> spc () ++ str "(decreasing respectively on " ++
@@ -422,21 +421,21 @@ let fixpoint_message indexes l =
 let cofixpoint_message l =
   Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "No corecursive definition.")
-  | [id] -> pr_id id ++ str " is corecursively defined"
-  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+  | [id] -> Id.print id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
                     spc () ++ str "are corecursively defined"))
 
 let recursive_message isfix i l =
   (if isfix then fixpoint_message i else cofixpoint_message) l
 
 let definition_message id =
-  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
 
 let assumption_message id =
   (* Changing "assumed" to "declared", "assuming" referring more to
   the type of the object than to the name of the object (see
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
-  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
 
 (** Global universe names, in a different summary *)
 
@@ -527,7 +526,7 @@ let do_constraint poly l =
        let names, _ = Global.global_universe_names () in
        try loc, Id.Map.find id names
        with Not_found ->
-         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
+         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id)
   in
   let in_section = Lib.sections_are_opened () in
   let () =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 72d22db4d..f70154e61 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Names
 open Globnames
-open Nameops
 open Term
 open Constr
 open Reduction
@@ -344,7 +343,7 @@ let check_correct_manual_implicits autoimps l =
     | ExplByName id,(b,fi,forced) ->
 	if not forced then
 	  user_err 
-            (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
+            (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".")
     | ExplByPos (i,_id),_t ->
 	if i<1 || i>List.length autoimps then
 	  user_err 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cae67c3e7..a5302b54d 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -29,11 +29,11 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
 let declare_generalizable_ident table (loc,id) =
   if not (Id.equal id (root_of_id id)) then
     user_err ?loc ~hdr:"declare_generalizable_ident"
-    ((pr_id id ++ str
+    ((Id.print id ++ str
       " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
   if Id.Pred.mem id table then
     user_err ?loc ~hdr:"declare_generalizable_ident"
-		((pr_id id++str" is already declared as a generalizable identifier"))
+		((Id.print id++str" is already declared as a generalizable identifier"))
   else Id.Pred.add id table
 
 let add_generalizable gen table =
@@ -80,7 +80,7 @@ let is_freevar ids env x =
 
 let ungeneralizable loc id =
   user_err ?loc ~hdr:"Generalization"
-	       (str "Unbound and ungeneralizable variable " ++ pr_id id)
+	       (str "Unbound and ungeneralizable variable " ++ Id.print id)
 
 let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let found loc id bdvars l =
@@ -152,7 +152,7 @@ let combine_params avoid fn applied needed =
             | Anonymous -> false
             in
 	    if not (List.exists is_id needed) then
-	      user_err ?loc  (str "Wrong argument name: " ++ Nameops.pr_id id);
+	      user_err ?loc  (str "Wrong argument name: " ++ Id.print id);
 	    true
 	| _ -> false) applied
   in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0967d21f0..0344dda97 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -239,7 +239,7 @@ let subtract_loc loc1 loc2 =
 
 let check_is_hole id t = match DAst.get t with GHole _ -> () | _ ->
   user_err ?loc:(loc_of_glob_constr t)
-   (strbrk "In recursive notation with binders, " ++ pr_id id ++
+   (strbrk "In recursive notation with binders, " ++ Id.print id ++
     strbrk " is expected to come without type.")
 
 let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
@@ -400,7 +400,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
   let vars = Id.Map.filter filter nenv.ninterp_var_type in
   let check_recvar x =
     if Id.List.mem x found then
-      user_err  (pr_id x ++
+      user_err  (Id.print x ++
 	strbrk " should only be used in the recursive part of a pattern.") in
   let check (x, y) = check_recvar x; check_recvar y in
   let () = List.iter check foundrec in
@@ -419,8 +419,8 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
   in
   let check_pair s x y where =
     if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
-      user_err  (strbrk "in the right-hand side, " ++ pr_id x ++
-	str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
+      user_err  (strbrk "in the right-hand side, " ++ Id.print x ++
+	str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++
 	str " position as part of a recursive pattern.") in
   let check_type x typ =
     match typ with
@@ -838,7 +838,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
       | Name id' ->
          if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in
     let unify_pat p p' =
-      if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p'
+      if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
       else raise No_match in
     let unify_term_binder c = DAst.(map (fun b' ->
       match DAst.get c, b' with
diff --git a/interp/reserve.ml b/interp/reserve.ml
index dc0f60dcf..6fd1d0b58 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -87,12 +87,12 @@ let in_reserved : Id.t * notation_constr -> obj =
 let declare_reserved_type_binding (loc,id) t =
   if not (Id.equal id (root_of_id id)) then
     user_err ?loc ~hdr:"declare_reserved_type"
-      ((pr_id id ++ str
+      ((Id.print id ++ str
       " is not reservable: it must have no trailing digits, quote, or _"));
   begin try
     let _ = Id.Map.find id !reserve_table in
     user_err ?loc ~hdr:"declare_reserved_type"
-    ((pr_id id++str" is already bound to a type"))
+    ((Id.print id++str" is already bound to a type"))
   with Not_found -> () end;
   add_anonymous_leaf (in_reserved (id,t))
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 84c6f4ef3..98e507309 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,16 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CErrors
 open Util
 open Pp
+open CErrors
 open Names
 open Libnames
-open Notation_term
 open Libobject
 open Lib
-open Nameops
 open Nametab
+open Notation_term
 
 (* Syntactic definitions. *)
 
@@ -31,7 +30,7 @@ let add_syntax_constant kn c onlyparse =
 let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
   if Nametab.exists_cci sp then
     user_err ~hdr:"cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
+      (Id.print (basename sp) ++ str " already exists");
   add_syntax_constant kn pat onlyparse;
   Nametab.push_syndef (Nametab.Until i) sp kn
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7a3c83ff9..c64d3aa26 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -186,14 +186,14 @@ let split_at_annot bl na =
 	| CLocalDef ((_,na),_,_) as x :: rest ->
            if Name.equal (Name id) na then
              user_err ?loc
-               (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+               (Id.print id ++ str" must be a proper parameter and not a local definition.")
            else
              aux (x :: acc) rest
         | CLocalPattern (_,_) :: rest ->
             Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
-            user_err ?loc 
-			 (str "No parameter named " ++ Nameops.pr_id id ++ str".")
+            user_err ?loc
+			 (str "No parameter named " ++ Id.print id ++ str".")
       in aux [] bl
 
 (* Used in correctness and interface *)