[api] Another large deprecation, `Nameops`

4 files changed, 23 insertions, 22 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ef7fac81..16798a1d5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -154,7 +154,7 @@ let error_incompatible_inst clenv mv  =
       Name id ->
         user_err ~hdr:"clenv_assign"
           (str "An incompatible instantiation has already been found for " ++
-           pr_id id)
+           Id.print id)
     | _ ->
         anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
 
@@ -417,7 +417,7 @@ let check_bindings bl =
   match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
     | NamedHyp s :: _ ->
 	user_err 
-	  (str "The variable " ++ pr_id s ++
+	  (str "The variable " ++ Id.print s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
 	user_err 
@@ -435,12 +435,12 @@ let explain_no_such_bound_variable evd id =
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
   user_err ~hdr:"Evd.meta_with_name"
-    (str"No such bound variable " ++ pr_id id ++
+    (str"No such bound variable " ++ Id.print id ++
      (if mvl == [] then str " (no bound variables at all in the expression)."
       else
         (str" (possible name" ++
          str (if List.length mvl == 1 then " is: " else "s are: ") ++
-         pr_enum pr_id mvl ++ str").")))
+         pr_enum Id.print mvl ++ str").")))
 
 let meta_with_name evd id =
   let na = Name id in
@@ -460,7 +460,7 @@ let meta_with_name evd id =
         n
     | _  ->
         user_err ~hdr:"Evd.meta_with_name"
-          (str "Binder name \"" ++ pr_id id ++
+          (str "Binder name \"" ++ Id.print id ++
            strbrk "\" occurs more than once in clause.")
 
 let meta_of_binder clause loc mvs = function
@@ -474,7 +474,7 @@ let error_already_defined b =
   match b with
     | NamedHyp id ->
         user_err 
-          (str "Binder name \"" ++ pr_id id ++
+          (str "Binder name \"" ++ Id.print id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
         anomaly
@@ -639,10 +639,10 @@ let explain_no_such_bound_variable holes id =
   let mvl = List.fold_right fold holes [] in
   let expl = match mvl with
   | [] -> str " (no bound variables at all in the expression)."
-  | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
-  | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
+  | [id] -> str "(possible name is: " ++ Id.print id ++ str ")."
+  | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")."
   in
-  user_err  (str "No such bound variable " ++ pr_id id ++ expl)
+  user_err  (str "No such bound variable " ++ Id.print id ++ expl)
 
 let evar_with_name holes id =
   let map h = match h.hole_name with
@@ -655,7 +655,7 @@ let evar_with_name holes id =
   | [h] -> h.hole_evar
   | _ ->
     user_err 
-      (str "Binder name \"" ++ pr_id id ++
+      (str "Binder name \"" ++ Id.print id ++
         str "\" occurs more than once in clause.")
 
 let evar_of_binder holes = function
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a633238f4..13a4e4ce3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -140,9 +140,9 @@ let reorder_context env sigma sign ord =
           let ((d,h),mh) = find_q top moved_hyps in
           if occur_vars_in_decl env sigma h d then
             user_err ~hdr:"reorder_context"
-              (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+              (str "Cannot move declaration " ++ Id.print top ++ spc() ++
               str "before " ++
-              pr_sequence pr_id
+              pr_sequence Id.print
                 (Id.Set.elements (Id.Set.inter h
                   (global_vars_set_of_decl env sigma d))));
           step ord' expected ctxt_head mh (d::ctxt_tail)
@@ -173,7 +173,7 @@ let check_decl_position env sigma sign d =
   let deps = dependency_closure env sigma (named_context_of_val sign) needed in
   if Id.List.mem x deps then
     user_err ~hdr:"Logic.check_decl_position"
-      (str "Cannot create self-referring hypothesis " ++ pr_id x);
+      (str "Cannot create self-referring hypothesis " ++ Id.print x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -234,10 +234,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location pr_id hto ++
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+	        Miscprint.pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
-	        ++ pr_id hyp ++ str ".")
+	        ++ Id.print hyp ++ str ".")
           else
 	    (d::first, middle)
 	in
@@ -507,10 +507,10 @@ let convert_hyp check sign sigma d =
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
 	  user_err ~hdr:"Logic.convert_hyp"
-            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
+            (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
 	  user_err ~hdr:"Logic.convert_hyp"
-            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
+            (str "Incorrect change of the body of "++ Id.print id ++ str ".");
        if check then reorder := check_decl_position env sigma sign d;
        map_named_decl EConstr.Unsafe.to_constr d) in
   reorder_val_context env sigma sign' !reorder
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 5d37c8a02..92b58b409 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Misctypes
 open Pp
+open Names
+open Misctypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,8 +19,8 @@ let rec pr_intro_pattern prc (_,pat) = match pat with
   | IntroAction p -> pr_intro_pattern_action prc p
 
 and pr_intro_pattern_naming = function
-  | IntroIdentifier id -> Nameops.pr_id id
-  | IntroFresh id -> str "?" ++ Nameops.pr_id id
+  | IntroIdentifier id -> Id.print id
+  | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
 
 and pr_intro_pattern_action prc = function
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 97faa1684..8b788bb38 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -185,7 +185,7 @@ let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (pr_sequence Nameops.pr_id l) ++ str".")
+               (pr_sequence Id.print l) ++ str".")
 
 let there_is_a_proof () = not (List.is_empty !pstates)
 let there_are_pending_proofs () = there_is_a_proof ()