Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.

13 files changed, 81 insertions, 83 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 3cf181441..9e63df51d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -19,7 +19,6 @@ open Termops
 open Declarations
 open Names
 open Globnames
-open Nameops
 open Inductiveops
 open Tactics
 open Ind_tables
@@ -361,7 +360,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
             else user_err ~hdr:"AutoIndDecl.do_replace_lb"
-                   (str "Var " ++ pr_id s ++ str " seems unknown.")
+                   (str "Var " ++ Id.print s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when CErrors.noncritical e ->
@@ -422,7 +421,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
             else user_err ~hdr:"AutoIndDecl.do_replace_bl"
-                   (str "Var " ++ pr_id s ++ str " seems unknown.")
+                   (str "Var " ++ Id.print s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when CErrors.noncritical e ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 22117f7e1..20cb43b24 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -180,7 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	Name id ->
 	  let sp = Lib.make_path id in
 	    if Nametab.exists_cci sp then
-	      user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+	      user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
 	    id
       | Anonymous ->
 	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
diff --git a/vernac/command.ml b/vernac/command.ml
index db3fa1955..be54f97b7 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -60,7 +60,7 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
       if not has_no_args then
 	user_err ?loc
 	 (strbrk"Cannot infer the non constant arguments of the conclusion of "
-	  ++ pr_id cs ++ str ".");
+	  ++ Id.print cs ++ str ".");
       let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in
       CAppExpl ((None,Ident(loc,name),None),List.rev args)
   | c -> c
@@ -181,7 +181,7 @@ match local with
   let () = assumption_message ident in
   let () =
     if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
-    Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
+    Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++
     strbrk " is not visible from current goals")
   in
   let r = VarRef ident in
@@ -328,9 +328,9 @@ type structured_inductive_expr =
 
 let minductive_message warn = function
   | []  -> user_err Pp.(str "No inductive definition.")
-  | [x] -> (pr_id x ++ str " is defined" ++ 
+  | [x] -> (Id.print x ++ str " is defined" ++ 
 	    if warn then str " as a non-primitive record" else 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 defined")
 
 let check_all_names_different indl =
@@ -764,11 +764,11 @@ let rec partial_order cmp = function
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if Id.List.mem x yge then
-      pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely"
+      Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely"
     else if Id.List.mem y xge then
-      pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely"
+      Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely"
     else
-      pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in
+      Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in
   let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in
   let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
diff --git a/vernac/command.mli b/vernac/command.mli
index 5415d3308..fb99a717b 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -127,24 +127,24 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+    recursive_preentry * Univdecls.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+  recursive_preentry * Univdecls.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
-  recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
+  recursive_preentry * Univdecls.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index d7a4fcca3..c18744052 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -11,18 +11,17 @@ open Declare
 open Entries
 open Globnames
 open Impargs
-open Nameops
 
 let warn_definition_not_visible =
   CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
     Pp.(fun ident ->
         strbrk "Section definition " ++
-        pr_id ident ++ strbrk " is not visible from current goals")
+        Names.Id.print ident ++ strbrk " is not visible from current goals")
 
 let warn_local_declaration =
   CWarnings.create ~name:"local-declaration" ~category:"scope"
     Pp.(fun (id,kind) ->
-        pr_id id ++ strbrk " is declared as a local " ++ str kind)
+        Names.Id.print id ++ strbrk " is declared as a local " ++ str kind)
 
 let get_locality id ~kind = function
 | Discharge ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 7b1a948ed..d15a811ba 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -159,7 +159,7 @@ let pr_explicit env sigma t1 t2 =
 let pr_db env i =
   try
     match env |> lookup_rel i |> get_name with
-      | Name id -> pr_id id
+      | Name id -> Id.print id
       | Anonymous -> str "<>"
   with Not_found -> str "UNBOUND_REL_" ++ int i
 
@@ -169,7 +169,7 @@ let explain_unbound_rel env sigma n =
   str "The reference " ++ int n ++ str " is free."
 
 let explain_unbound_var env v =
-  let var = pr_id v in
+  let var = Id.print v in
   str "No such section variable or assumption: " ++ var ++ str "."
 
 let explain_not_type env sigma j =
@@ -189,7 +189,7 @@ let explain_bad_assumption env sigma j =
 let explain_reference_variables sigma id c =
   (* c is intended to be a global reference *)
   let pc = pr_global (fst (Termops.global_of_constr sigma c)) in
-  pc ++ strbrk " depends on the variable " ++ pr_id id ++
+  pc ++ strbrk " depends on the variable " ++ Id.print id ++
   strbrk " which is not declared in the context."
 
 let rec pr_disjunction pr = function
@@ -415,7 +415,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
   let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in
   let prt_name i =
     match names.(i) with
-        Name id -> str "Recursive definition of " ++ pr_id id
+        Name id -> str "Recursive definition of " ++ Id.print id
       | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in
 
   let st = match err with
@@ -430,7 +430,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
       let arg_env = make_all_name_different arg_env sigma in
       let called =
         match names.(j) with
-            Name id -> pr_id id
+            Name id -> Id.print id
           | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
       let pr_db x = quote (pr_db env x) in
       let vars =
@@ -450,7 +450,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
   | NotEnoughArgumentsForFixCall j ->
       let called =
         match names.(j) with
-            Name id -> pr_id id
+            Name id -> Id.print id
           | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
      str "Recursive call to " ++ called ++ str " has not enough arguments"
 
@@ -528,7 +528,7 @@ let pr_trailing_ne_context_of env sigma =
 
 let rec explain_evar_kind env sigma evk ty = function
   | Evar_kinds.NamedHole id ->
-      strbrk "the existential variable named " ++ pr_id id
+      strbrk "the existential variable named " ++ Id.print id
   | Evar_kinds.QuestionMark _ ->
       strbrk "this placeholder of type " ++ ty
   | Evar_kinds.CasesType false ->
@@ -537,12 +537,12 @@ let rec explain_evar_kind env sigma evk ty = function
       strbrk "a subterm of type " ++ ty ++
       strbrk " in the type of this pattern-matching problem"
   | Evar_kinds.BinderType (Name id) ->
-      strbrk "the type of " ++ Nameops.pr_id id
+      strbrk "the type of " ++ Id.print id
   | Evar_kinds.BinderType Anonymous ->
       strbrk "the type of this anonymous binder"
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
-      strbrk "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++
+      strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++
       spc () ++ Nametab.pr_global_env Id.Set.empty c ++
       strbrk " whose type is " ++ ty
   | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty
@@ -558,7 +558,7 @@ let rec explain_evar_kind env sigma evk ty = function
       assert false
   | Evar_kinds.VarInstance id ->
       strbrk "an instance of type " ++ ty ++
-      str " for the variable " ++ pr_id id
+      str " for the variable " ++ Id.print id
   | Evar_kinds.SubEvar evk' ->
       let evi = Evd.find sigma evk' in
       let pc = match evi.evar_body with
@@ -598,7 +598,7 @@ let explain_unsolvable_implicit env sigma evk explain =
   explain_placeholder_kind env sigma evi.evar_concl explain ++ pe
 
 let explain_var_not_found env id =
-  str "The variable" ++ spc () ++ pr_id id ++
+  str "The variable" ++ spc () ++ Id.print id ++
   spc () ++ str "was not found" ++
   spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."
 
@@ -638,7 +638,7 @@ let explain_no_occurrence_found env sigma c id =
   str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
   str " in " ++
     (match id with
-      | Some id -> pr_id id
+      | Some id -> Id.print id
       | None -> str"the current goal") ++ str "."
 
 let explain_cannot_unify_binding_type env sigma m n =
@@ -660,7 +660,7 @@ let explain_wrong_abstraction_type env sigma na abs expected result =
   let abs = EConstr.to_constr sigma abs in
   let expected = EConstr.to_constr sigma expected in
   let result = EConstr.to_constr sigma result in
-  let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in
+  let ppname = match na with Name id -> Id.print id ++ spc () | _ -> mt () in
   str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++
   pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++
   pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++
@@ -723,9 +723,9 @@ let explain_type_error env sigma err =
 let pr_position (cl,pos) =
   let clpos = match cl with
     | None -> str " of the goal"
-    | Some (id,Locus.InHyp) -> str " of hypothesis " ++ pr_id id
-    | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
-    | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
+    | Some (id,Locus.InHyp) -> str " of hypothesis " ++ Id.print id
+    | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ Id.print id
+    | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ Id.print id in
   int pos ++ clpos
 
 let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) e =
@@ -844,7 +844,7 @@ let explain_not_match_error = function
   | ModuleTypeFieldExpected ->
     strbrk "a module type is expected"
   | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
-    str "types given to " ++ pr_id id ++ str " differ"
+    str "types given to " ++ Id.print id ++ str " differ"
   | NotConvertibleBodyField ->
     str "the body of definitions differs"
   | NotConvertibleTypeField (env, typ1, typ2) ->
@@ -869,7 +869,7 @@ let explain_not_match_error = function
   | RecordProjectionsExpected nal ->
     (if List.length nal >= 2 then str "expected projection names are "
      else str "expected projection name is ") ++
-    pr_enum (function Name id -> pr_id id | _ -> str "_") nal
+    pr_enum (function Name id -> Id.print id | _ -> str "_") nal
   | NotEqualInductiveAliases ->
     str "Aliases to inductive types do not match"
   | NoTypeConstraintExpected ->
@@ -1016,7 +1016,7 @@ let explain_not_a_class env c =
   pr_constr_env env Evd.empty c ++ str" is not a declared type class."
 
 let explain_unbound_method env cid id =
-  str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++
+  str "Unbound method name " ++ Id.print (snd id) ++ spc () ++
   str"of class" ++ spc () ++ pr_global cid ++ str "."
 
 let pr_constr_exprs exprs =
@@ -1061,7 +1061,7 @@ let explain_intro_needs_product () =
 
 let explain_does_not_occur_in c hyp =
   str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++
-  str "does not occur in" ++ spc () ++ pr_id hyp ++ str "."
+  str "does not occur in" ++ spc () ++ Id.print hyp ++ str "."
 
 let explain_non_linear_proof c =
   str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
@@ -1072,7 +1072,7 @@ let explain_meta_in_type c =
   str " of another meta"
 
 let explain_no_such_hyp id =
-  str "No such hypothesis: " ++ pr_id id
+  str "No such hypothesis: " ++ Id.print id
 
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
@@ -1102,7 +1102,7 @@ let error_ill_formed_inductive env c v =
 let error_ill_formed_constructor env id c v nparams nargs =
   let pv = pr_lconstr_env env Evd.empty v in
   let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
-  str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++
+  str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++
   str "is not valid;" ++ brk(1,1) ++
   strbrk (if atomic then "it must be " else "its conclusion must be ") ++
   pv ++
@@ -1130,17 +1130,17 @@ let error_bad_ind_parameters env c n v1 v2  =
   str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
 
 let error_same_names_types id =
-  str "The name" ++ spc () ++ pr_id id ++ spc () ++
+  str "The name" ++ spc () ++ Id.print id ++ spc () ++
   str "is used more than once."
 
 let error_same_names_constructors id =
-  str "The constructor name" ++ spc () ++ pr_id id ++ spc () ++
+  str "The constructor name" ++ spc () ++ Id.print id ++ spc () ++
   str "is used more than once."
 
 let error_same_names_overlap idl =
   strbrk "The following names are used both as type names and constructor " ++
   str "names:" ++ spc () ++
-  prlist_with_sep pr_comma pr_id idl ++ str "."
+  prlist_with_sep pr_comma Id.print idl ++ str "."
 
 let error_not_an_arity env c =
   str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index be9de5b30..7b8a38d5f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -217,7 +217,7 @@ let compute_proof_name locality = function
       if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
-        user_err ?loc  (pr_id id ++ str " already exists.");
+        user_err ?loc  (Id.print id ++ str " already exists.");
       id
   | None ->
     let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
@@ -294,7 +294,7 @@ let save_anonymous ?export_seff proof save_ident =
 
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
+                   (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
                                 spc () ++ strbrk "declared as an axiom.")
 
 let admit (id,k,e) pl hook () =
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1f46a385d..6972edd52 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -27,10 +27,10 @@ val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_m
    unit declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
-  ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+  ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
-  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
+  (UState.t option -> unit declaration_hook) -> unit
 
 val start_proof_com :
   ?inference_hook:Pretyping.inference_hook ->
@@ -46,7 +46,7 @@ val start_proof_with_initialization :
 
 val universe_proof_terminator :
   Proof_global.lemma_possible_guards ->
-    (Evd.evar_universe_context option -> unit declaration_hook) ->
+    (UState.t option -> unit declaration_hook) ->
     Proof_global.proof_terminator
 
 val standard_proof_terminator :
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 9376afa8c..6c3dfec7d 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -310,7 +310,7 @@ let rec get_notation_vars onlyprint = function
 	(* don't check for nonlinearity if printing only, see Bug 5526 *)
 	if not onlyprint && Id.List.mem id vars then 
 	  user_err ~hdr:"Metasyntax.get_notation_vars"
-            (str "Variable " ++ pr_id id ++ str " occurs more than once.")
+            (str "Variable " ++ Id.print id ++ str " occurs more than once.")
 	else id::vars
   | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
   | SProdList _ :: _ -> assert false
@@ -323,7 +323,7 @@ let analyze_notation_tokens ~onlyprint l =
 
 let error_not_same_scope x y =
   user_err ~hdr:"Metasyntax.error_not_name_scope"
-    (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
+    (str "Variables " ++ Id.print x ++ str " and " ++ Id.print y ++ str " must be in the same scope.")
 
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
@@ -398,7 +398,7 @@ let check_open_binder isopen sl m =
   | _ -> assert false
   in
   if isopen && not (List.is_empty sl) then
-    user_err  (str "as " ++ pr_id m ++
+    user_err  (str "as " ++ Id.print m ++
       str " is a non-closed binder, no such \"" ++
       prlist_with_sep spc pr_token sl
       ++ strbrk "\" is allowed to occur.")
@@ -865,7 +865,7 @@ let check_useless_entry_types recvars mainvars etyps =
   let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
   match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
   | (x,_)::_ -> user_err ~hdr:"Metasyntax.check_useless_entry_types"
-                  (pr_id x ++ str " is unbound in the notation.")
+                  (Id.print x ++ str " is unbound in the notation.")
   | _ -> ()
 
 let check_binder_type recvars etyps =
@@ -922,7 +922,7 @@ let join_auxiliary_recursive_types recvars etyps =
     | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
     | Some xtyp, Some ytyp ->
 	user_err 
-	  (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
+	  (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++
 	   strbrk ", both ends have incompatible types."))
     recvars etyps
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e23146273..ed4d8b888 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -304,7 +304,7 @@ type program_info_aux = {
   prg_name: Id.t;
   prg_body: constr;
   prg_type: constr;
-  prg_ctx:  Evd.evar_universe_context;
+  prg_ctx:  UState.t;
   prg_univdecl: Univdecls.universe_decl;
   prg_obligations: obligations;
   prg_deps : Id.t list;
@@ -313,7 +313,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
+  prg_hook : (UState.t -> unit) Lemmas.declaration_hook;
   prg_opaque : bool;
   prg_sign: named_context_val;
 }
@@ -437,7 +437,7 @@ let close sec =
     let keys = map_keys !from_prg in
       user_err ~hdr:"Program" 
 	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
-	   prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
+	   prlist_with_sep spc (fun x -> Id.print x) keys ++
 	   (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
 	      str "unsolved obligations"))
 
@@ -716,10 +716,10 @@ let get_prog name =
 	       | _ ->
                 let progs = Id.Set.elements (ProgMap.domain prg_infos) in
                 let prog = List.hd progs in
-                let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
+                let progs = prlist_with_sep pr_comma Id.print progs in
                 user_err 
                   (str "More than one program with unsolved obligations: " ++ progs
-                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
+                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\""))
 
 let get_any_prog () =
   let prg_infos = !from_prg in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index d037fdcd8..481faadb8 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -52,13 +52,13 @@ type progress = (* Resolution status of a program *)
 val default_tactic : unit Proofview.tactic ref
 
 val add_definition : Names.Id.t -> ?term:constr -> types -> 
-  Evd.evar_universe_context ->
+  UState.t ->
   ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(constr -> constr) ->
-  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -70,12 +70,12 @@ type fixpoint_kind =
 val add_mutual_definitions :
   (Names.Id.t * constr * types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
-  Evd.evar_universe_context ->
+  UState.t ->
   ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 1fd43624a..1bd47a556 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -138,7 +138,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
   let arity = EConstr.it_mkProd_or_LetIn typ newps in
   let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
   let assums = List.filter is_local_assum newps in
-  let params = List.map (RelDecl.get_name %> out_name) assums in
+  let params = List.map (RelDecl.get_name %> Name.get_id) assums in
   let ty = Inductive (params,(finite != BiFinite)) in
   let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in
   let env2,impls,newfs,data =
@@ -194,24 +194,24 @@ let warning_or_error coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
 	let s,have = if List.length projs > 1 then "s","were" else "","was" in
-        (pr_id fi ++
+        (Id.print fi ++
 	   strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
-           prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++
+           prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++
 	   strbrk " not defined.")
     | BadTypedProj (fi,ctx,te) ->
 	match te with
 	  | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
-              (pr_id fi ++
+              (Id.print fi ++
 		strbrk" cannot be defined because it is informative and " ++
 		Printer.pr_inductive (Global.env()) indsp ++
 		strbrk " is not.")
 	  | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
-	      (pr_id fi ++
+	      (Id.print fi ++
 		strbrk" cannot be defined because it is large and " ++
 		Printer.pr_inductive (Global.env()) indsp ++
 		strbrk " is not.")
 	  | _ ->
-              (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
+              (Id.print fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then user_err ~hdr:"structure" st;
   warn_cannot_define_projection (hov 0 st)
@@ -240,7 +240,7 @@ let subst_projection fid l c =
 	    | Projection t -> lift depth t
 	    | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
 	    | NoProjection Anonymous ->
-                user_err  (str "Field " ++ pr_id fid ++
+                user_err  (str "Field " ++ Id.print fid ++
                   str " depends on the " ++ pr_nth (k-depth-1) ++ str
                   " field which has no name.")
         else
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7eedf24f8..5bcb3b1e1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -84,10 +84,10 @@ let show_intro all =
     let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
     if all then
       let lid = Tactics.find_intro_names l gl in
-      Feedback.msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
+      Feedback.msg_notice (hov 0 (prlist_with_sep  spc Id.print lid))
     else if not (List.is_empty l) then
       let n = List.last l in
-      Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+      Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl)))
   end
 
 (** Prepare a "match" template for a given inductive type.
@@ -252,7 +252,7 @@ let print_namespace ns =
     (* spiwack: I'm ignoring the dirpath, is that bad? *)
     let (mp,_,lbl) = Names.KerName.repr kn in
     let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
-    print_list pr_id qn
+    print_list Id.print qn
   in
   let print_constant k body =
     (* FIXME: universes *)
@@ -272,7 +272,7 @@ let print_namespace ns =
         acc
     ) constants (str"")
   in
-  Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
+  Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace)
 
 let print_strategy r =
   let open Conv_oracle in
@@ -656,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
       id binders_ast (Enforce mty_ast) []
   in
   Dumpglob.dump_moddef ?loc mp "mod";
-  Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
+  Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -678,7 +678,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
-         (str "Interactive Module " ++ pr_id id ++ str " started");
+         (str "Interactive Module " ++ Id.print id ++ str " started");
        List.iter
          (fun (export,id) ->
            Option.iter
@@ -696,14 +696,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
-	 (str "Module " ++ pr_id id ++ str " is defined");
+	 (str "Module " ++ Id.print id ++ str " is defined");
        Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
          export
 
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref ?loc mp "mod";
-  Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
+  Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -725,7 +725,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
        in
        Dumpglob.dump_moddef ?loc mp "modtype";
        Flags.if_verbose Feedback.msg_info
-	 (str "Interactive Module Type " ++ pr_id id ++ str " started");
+	 (str "Interactive Module Type " ++ Id.print id ++ str " started");
        List.iter
          (fun (export,id) ->
            Option.iter
@@ -744,12 +744,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
         in
         Dumpglob.dump_moddef ?loc mp "modtype";
 	Flags.if_verbose Feedback.msg_info
-	  (str "Module Type " ++ pr_id id ++ str " is defined")
+	  (str "Module Type " ++ Id.print id ++ str " is defined")
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref ?loc mp "modtype";
-  Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined")
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_module_ast l
@@ -874,7 +874,7 @@ let vernac_set_used_variables e =
   List.iter (fun id -> 
     if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
       user_err ~hdr:"vernac_set_used_variables"
-        (str "Unknown variable: " ++ pr_id id))
+        (str "Unknown variable: " ++ Id.print id))
     l;
   let _, to_clear = Proof_global.set_used_variables l in
   let to_clear = List.map snd to_clear in
@@ -1628,7 +1628,7 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    v 0 (pr_id id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
+    v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
     | NoHyp | Not_found -> print_about ref_or_by_not
@@ -1859,7 +1859,7 @@ let vernac_show = let open Feedback in function
   | ShowExistentials -> show_top_evars ()
   | ShowUniverses -> show_universes ()
   | ShowProofNames ->
-      msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names()))
+      msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id