Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.

34 files changed, 255 insertions, 152 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7fad65bf0a..3f3b0a870a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,6 +51,12 @@ In Constrexpr_ops:
   interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
   ones were preserving the original sharing of the type.
 
+In Nameops:
+
+  The API has been made more uniform. New combinators added in the
+  "Name" space name. Function "out_name" now fails with IsAnonymous
+  rather than with Failure "Nameops.out_name".
+
 Location handling and AST attributes:
 
   Location handling has been reworked. First, Loc.ghost has been
diff --git a/engine/termops.ml b/engine/termops.ml
index ca32c06a75..1af9bd1ffc 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -31,10 +31,6 @@ let pr_sort_family = function
   | InProp -> (str "Prop")
   | InType -> (str "Type")
 
-let pr_name = function
-  | Name id -> pr_id id
-  | Anonymous -> str "_"
-
 let pr_con sp = str(string_of_con sp)
 
 let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
@@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
   hov 1
       (str"fix " ++ int i ++ spc() ++  str"{" ++
          v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
-           pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+           Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
 	   cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
@@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with
       (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
        pr_constr c ++ str")")
   | Lambda (na,t,c) -> hov 1
-      (str"fun " ++ pr_name na ++ str":" ++
+      (str"fun " ++ Name.print na ++ str":" ++
        pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
   | LetIn (na,b,t,c) -> hov 0
-      (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
+      (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++
        str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
        pr_constr c)
   | App (c,l) ->  hov 1
@@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with
       hov 1
         (str"cofix " ++ int i ++ spc() ++  str"{" ++
          v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
-           pr_name na ++ str":" ++ pr_constr ty ++
+           Name.print na ++ str":" ++ pr_constr ty ++
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
@@ -308,8 +304,8 @@ let pr_evar_universe_context ctx =
 let print_env_short env =
   let print_constr = print_kconstr in
   let pr_rel_decl = function
-    | RelDecl.LocalAssum (n,_) -> pr_name n
-    | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+    | RelDecl.LocalAssum (n,_) -> Name.print n
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")"
   in
   let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4c29fc8097..f6da10c961 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -740,7 +740,7 @@ let rec extern inctx scopes vars r =
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
-      List.fold_right (name_fold Id.Set.add)
+      List.fold_right (Name.fold_right Id.Set.add)
 	(cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
@@ -790,12 +790,12 @@ let rec extern inctx scopes vars r =
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
-                 let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
+                 let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
+                 let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
-		     | Some x -> Some (Loc.tag @@ out_name (List.nth assums x))
+		     | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x))
 		 in
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
 		 ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
@@ -807,8 +807,8 @@ let rec extern inctx scopes vars r =
                Array.mapi (fun i fi ->
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
-                 let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
+                 let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
+                 let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
 		 ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
@@ -852,14 +852,14 @@ and extern_local_binder scopes vars = function
     [] -> ([],[],[])
   | { v = GLocalDef (na,bk,bd,ty)}::l ->
       let (assums,ids,l) =
-        extern_local_binder scopes (name_fold Id.Set.add na vars) l in
+        extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
       (assums,na::ids,
        CLocalDef((Loc.tag na), extern false scopes vars bd,
                    Option.map (extern false scopes vars) ty) :: l)
 
   | { v = GLocalAssum (na,bk,ty)}::l ->
       let ty = extern_typ scopes vars ty in
-      (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
+      (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
           (assums,ids,CLocalAssum(nal,k,ty')::l)
             when constr_expr_eq ty ty' &&
               match na with Name id -> not (occur_var_constr_expr id ty')
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d5d8e8658..b8d333f0d0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,na = coerce_to_name (fst (Id.Map.find id terms)) in
-    (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na
+    (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
-            (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
+            (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na)
 	    inb) Id.Set.empty tms in
         (* as, in & return vars *)
         let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cfc6e6c2a6..ade524141a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -264,7 +264,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
             let () = match bk with
             | Implicit ->
 	       Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ 
-			      pr_name na ++ strbrk " and following binders")
+			      Name.print na ++ strbrk " and following binders")
             | _ -> ()
             in []
       | GLambda (na, bk, t, b) -> abs na bk b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6f91009111..ec8fa498ca 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -184,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 	  e',Some (Loc.tag ?loc (ind,nal')) in
 	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
+      let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
 	  List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a79f10df6b..94bbc60eaf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms =
     (fun (_, ona, indnal) l ->
       Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
       indnal
-        (Option.fold_right (down_located (name_fold Id.Set.add)) ona l))
+        (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
-      let n' = List.fold_right (name_fold g) nal n in
+      let n' = List.fold_right (Name.fold_right g) nal n in
       f n (fold_constr_expr_binders g f n' acc b l) t
   | [] ->
       f n acc b
@@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function
 let rec fold_local_binders g f n acc b = function
   | CLocalAssum (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
-      let n' = List.fold_right (name_fold g) nal n in
+      let n' = List.fold_right (Name.fold_right g) nal n in
       f n (fold_local_binders g f n' acc b l) t
   | CLocalDef ((_,na),c,t)::l ->
-      Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
+      Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
   | CLocalPattern (_,(pat,t))::l ->
       let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
       Option.fold_left (f n) acc t
@@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
   | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
   | CLetIn (na,a,t,b) ->
-     f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+     f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
   | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
   | CCast (a,CastCoerce) -> f n acc a
   | CNotation (_,(l,ll,bll)) ->
@@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
   | CLetTuple (nal,(ona,po),b,c) ->
-      let n' = List.fold_right (down_located (name_fold g)) nal n in
-      f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
+      let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
+      f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
   | CIf (c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
-	(f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
+	(f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po
   | CFix (_,l) ->
       let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -198,7 +198,7 @@ let split_at_annot bl na =
 
 (* Used in correctness and interface *)
 
-let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
+let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -212,7 +212,7 @@ let map_local_binders f g e bl =
       CLocalAssum(nal,k,ty) ->
         (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
     | CLocalDef((loc,na),c,ty) ->
-        (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
+        (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
     | CLocalPattern (loc,(pat,t)) ->
         let ids = ids_of_pattern pat in
         (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
@@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
   | CLambdaN (bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
   | CLetIn (na,a,t,b) ->
-      CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
+      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
   | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
   | CNotation (n,(l,ll,bll)) ->
       (* This is an approximation because we don't know what binds what *)
@@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (nal,(ona,po),b,c) ->
-      let e' = List.fold_right (down_located (name_fold g)) nal e in
-      let e'' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
+      let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
       CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
   | CIf (c,(ona,po),b1,b2) ->
-      let e' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
   | CFix (id,dl) ->
       CFix (id,List.map (fun (id,n,bl,t,d) ->
diff --git a/kernel/names.ml b/kernel/names.ml
index afdbe0c0dc..ae34033355 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -104,8 +104,12 @@ struct
     | _ -> false
 
   let hash = function
-  | Anonymous -> 0
-  | Name id -> Id.hash id
+    | Anonymous -> 0
+    | Name id -> Id.hash id
+
+  let print = function
+    | Anonymous -> str "_"
+    | Name id -> Id.print id
 
   module Self_Hashcons =
     struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 5b0163aa55..c73eb197bb 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -105,6 +105,9 @@ sig
   val hcons : t -> t
   (** Hashconsing over names. *)
 
+  val print : t -> Pp.std_ppcmds
+  (** Pretty-printer (print "_" for [Anonymous]. *)
+
 end
 
 (** {6 Type aliases} *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 098f5112fd..b73bd7eb38 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -14,10 +14,6 @@ open Names
 
 let pr_id id = Id.print id
 
-let pr_name = function
-  | Anonymous -> str "_"
-  | Name id -> pr_id id
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -124,34 +120,82 @@ let atompart_of_id id = fst (repr_ident id)
 
 (* Names *)
 
-let out_name = function
-  | Name id -> id
-  | Anonymous -> failwith "Nameops.out_name"
+module type ExtName =
+sig
+
+  include module type of struct include Names.Name end
+
+  exception IsAnonymous
+
+  val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a
+  val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
+  val iter : (Id.t -> unit) -> t -> unit
+  val map : (Id.t -> Id.t) -> t -> t
+  val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+  val get_id : t -> Id.t
+  val pick : t -> t -> t
+  val cons : t -> Id.t list -> Id.t list
+  val to_option : Name.t -> Id.t option
+
+end
+
+module Name : ExtName =
+struct
+
+  include Names.Name
+
+  exception IsAnonymous
+
+  let fold_left f a = function
+    | Name id -> f a id
+    | Anonymous -> a
+
+  let fold_right f na a =
+    match na with
+    | Name id -> f id a
+    | Anonymous -> a
+
+  let iter f na = fold_right (fun x () -> f x) na ()
+
+  let map f = function
+    | Name id -> Name (f id)
+    | Anonymous -> Anonymous
+
+  let fold_map f a = function
+    | Name id -> let (a, id) = f a id in (a, Name id)
+    | Anonymous -> a, Anonymous
+
+  let get_id = function
+    | Name id -> id
+    | Anonymous -> raise IsAnonymous
 
-let name_fold f na a =
-  match na with
-  | Name id -> f id a
-  | Anonymous -> a
+  let pick na1 na2 =
+    match na1 with
+    | Name _ -> na1
+    | Anonymous -> na2
 
-let name_iter f na = name_fold (fun x () -> f x) na ()
+  let cons na l =
+    match na with
+    | Anonymous -> l
+    | Name id -> id::l
 
-let name_cons na l =
-  match na with
-  | Anonymous -> l
-  | Name id -> id::l
+  let to_option = function
+    | Anonymous -> None
+    | Name id -> Some id
 
-let name_app f = function
-  | Name id -> Name (f id)
-  | Anonymous -> Anonymous
+end
 
-let name_fold_map f e = function
-  | Name id -> let (e,id) = f e id in (e,Name id)
-  | Anonymous -> e,Anonymous
+open Name
 
-let name_max na1 na2 =
-  match na1 with
-  | Name _ -> na1
-  | Anonymous -> na2
+(* Compatibility *)
+let out_name = get_id
+let name_fold = fold_right
+let name_iter = iter
+let name_app = map
+let name_fold_map = fold_map
+let name_cons = cons
+let name_max = pick
+let pr_name = print
 
 let pr_lab l = Label.print l
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 3a67b61a13..abfc09db8d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -9,8 +9,6 @@
 open Names
 
 (** Identifiers and names *)
-val pr_id : Id.t -> Pp.std_ppcmds
-val pr_name : Name.t -> Pp.std_ppcmds
 
 val make_ident : string -> int option -> Id.t
 val repr_ident : Id.t -> string * int option
@@ -50,16 +48,69 @@ val increment_subscript : Id.t -> Id.t
 
 val forget_subscript    : Id.t -> Id.t
 
+module Name : sig
+
+  include module type of struct include Names.Name end
+
+  exception IsAnonymous
+
+  val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a
+  (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *)
+
+  val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+  (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *)
+
+  val iter : (Id.t -> unit) -> Name.t -> unit
+  (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *)
+
+  val map : (Id.t -> Id.t) -> Name.t -> t
+  (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)
+
+  val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+  (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
+      It is [a,Anonymous] otherwise. *)
+
+  val get_id : Name.t -> Id.t
+  (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
+
+  val pick : Name.t -> Name.t -> Name.t
+  (** [pick na na'] returns [Anonymous] if both names are [Anonymous].
+      Pick one of [na] or [na'] otherwise. *)
+
+  val cons : Name.t -> Id.t list -> Id.t list
+  (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
+
+  val to_option : Name.t -> Id.t option
+  (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *)
+
+end
+
 val out_name : Name.t -> Id.t
-(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
-    otherwise. *)
+(** @deprecated Same as [Name.get_id] *)
 
 val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+(** @deprecated Same as [Name.fold_right] *)
+
 val name_iter : (Id.t -> unit) -> Name.t -> unit
-val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.iter] *)
+
 val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
+(** @deprecated Same as [Name.map] *)
+
 val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+(** @deprecated Same as [Name.fold_map] *)
+
 val name_max : Name.t -> Name.t -> Name.t
+(** @deprecated Same as [Name.pick] *)
+
+val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.cons] *)
+
+val pr_name : Name.t -> Pp.std_ppcmds
+(** @deprecated Same as [Name.print] *)
+
+val pr_id : Id.t -> Pp.std_ppcmds
+(** @deprecated Same as [Names.Id.print] *)
 
 val pr_lab : Label.t -> Pp.std_ppcmds
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 434fb14a6e..0041797de7 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -944,7 +944,7 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
 let var_of_decl = id_of_decl %> mkVar
 let revert idl =
   tclTHEN
@@ -1127,11 +1127,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1158,7 +1158,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		(fun i types ->
 		   let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
-		     name = Nameops.out_name (fresh_id names.(i));
+		     name = Nameops.Name.get_id (fresh_id names.(i));
 		     types = types;
 		     offset = fix_offset;
 		     nb_realargs =
@@ -1181,7 +1181,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
 		   let app_f = mkApp(f,first_args) in
 		   let pte_args = (Array.to_list first_args)@[app_f] in
-		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
+		   let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
@@ -1208,9 +1208,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 			 num_in_block = num
 		     }
 		   in
-(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
+(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++  *)
 (* 			      str " to " ++ Ppconstr.pr_id info.name); *)
-		   (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info)
 		   )
 		0
 		(Id.Map.empty,[])
@@ -1284,7 +1284,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
+			  (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1563,17 +1563,17 @@ let prove_principle_for_gen
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
-  let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
+  let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
   let acc_rec_arg_id =
-    Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
+    Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
     tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
-  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+  let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
@@ -1591,7 +1591,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
+  let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
@@ -1639,7 +1639,7 @@ let prove_principle_for_gen
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (get_name %> Nameops.out_name)
+	(List.rev_map (get_name %> Nameops.Name.get_id)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1677,14 +1677,14 @@ let prove_principle_for_gen
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
 	 let predicates_names =
-	   List.map (get_name %> Nameops.out_name) princ_info.predicates
+	   List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
 	       (fun eqs ->
 (* 		  msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id  !tcc_list); *)
-(* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
-(* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
+(* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+(* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
 (* 		  msgnl (str "acc_rec_arg_id := "++  Ppconstr.pr_id acc_rec_arg_id); *)
 (* 		  msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id  eqs); *)
 
@@ -1693,7 +1693,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (get_name %> Nameops.out_name)
+			   (get_name %> Nameops.Name.get_id)
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1722,7 +1722,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (get_name %> Nameops.out_name) princ_info.branches)
+	      (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 18d63dd94b..9425271671 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       then List.tl args
       else args
     in
-    Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
+    Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
                                           Term.compose_prod real_args (mkSort new_sort))
   in
   let new_predicates =
@@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
        with
 	 | Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
 	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
@@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
       with
 	| Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
 	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 74c0eb4cc7..4946285e16 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -200,13 +200,13 @@ let is_rec names =
     | GIf(b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | GProd(na,_,t,b) | GLambda(na,_,t,b) ->
-	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
+	lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
     | GLetIn(na,b,t,c) ->
-	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
+	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
     | GLetTuple(nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
-	     (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
+	     (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
 	     names
 	     nal
 	  )
@@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) -> CAst.make ?loc @@ 
-					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
+					   CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
 			       )
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d68bdc2153..12232dd83d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -421,7 +421,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
 	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -431,7 +431,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
 	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2f9f708768..62eba9513d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -879,7 +879,7 @@ let rec make_rewrite_list expr_info max = function
 	    let k_na,_,t = destProd sigma t_eq in
 	    let _,_,t  = destProd sigma t in
 	    let def_na,_,_ = destProd sigma t in
-	    Nameops.out_name k_na,Nameops.out_name def_na
+	    Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
 	  in
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
@@ -905,7 +905,7 @@ let make_rewrite expr_info l hp max =
 	    let k_na,_,t = destProd sigma t_eq in
 	    let _,_,t  = destProd sigma t in
 	    let def_na,_,_ = destProd sigma t in
-	    Nameops.out_name k_na,Nameops.out_name def_na
+	    Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
 	  in
 	 observe_tac (str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2ba..67d2b452ac 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -571,7 +571,7 @@ type 'a extra_genarg_printer =
               str "=>" ++ brk (1,4) ++ pr t))
     | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
-  let pr_funvar n = spc () ++ pr_name n
+  let pr_funvar n = spc () ++ Name.print n
 
   let pr_let_clause k pr (id,(bl,t)) =
     hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 75f89a81e1..f44ccbd3b5 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -502,7 +502,7 @@ let print_ltacs () =
     | Tacexpr.TacFun (l, t) -> (l, t)
     | _ -> ([], body)
     in
-    let pr_ltac_fun_arg n = spc () ++ pr_name n in
+    let pr_ltac_fun_arg n = spc () ++ Name.print n in
     hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e431a13bc2..82711dd46a 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -718,7 +718,7 @@ let split_ltac_fun = function
   | TacFun (l,t) -> (l,t)
   | t -> ([],t)
 
-let pr_ltac_fun_arg n = spc () ++ pr_name n
+let pr_ltac_fun_arg n = spc () ++ Name.print n
 
 let print_ltac id =
  try
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d11..31c1b79ee0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1116,11 +1116,11 @@ let cons_and_check_name id l =
 
 let rec read_match_goal_hyps lfun ist env sigma lidh = function
   | (Hyp ((loc,na) as locna,mp))::tl ->
-      let lidh' = name_fold cons_and_check_name na lidh in
+      let lidh' = Name.fold_right cons_and_check_name na lidh in
       Hyp (locna,read_pattern lfun ist env sigma mp)::
 	(read_match_goal_hyps lfun ist env sigma lidh' tl)
   | (Def ((loc,na) as locna,mv,mp))::tl ->
-      let lidh' = name_fold cons_and_check_name na lidh in
+      let lidh' = Name.fold_right cons_and_check_name na lidh in
       Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
 	(read_match_goal_hyps lfun ist env sigma lidh' tl)
   | [] -> []
@@ -1423,7 +1423,7 @@ and tactic_of_value ist vle =
       (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
        Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
        Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
-       pr_enum pr_name vars ++ Pp.str ".")
+       pr_enum Name.print vars ++ Pp.str ".")
   | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a98..f16f393f60 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -731,7 +731,7 @@ let get_names env sigma sign eqns =
 	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
 	     d na
 	 in
-         (na::l,(out_name na)::avoid))
+         (na::l,(Name.get_id na)::avoid))
       ([],allvars) (List.rev sign) names2 in
   names3,aliasname
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 752819aa39..6f099c8dfd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs =
       let nal,c = it_destRLambda_or_LetIn_names n b in
       let mkPatVar na = CAst.make @@ PatVar na in
       let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
-      let map name = try Some (Nameops.out_name name) with Failure _ -> None in
-      let ids = List.map_filter map nal in
+      let ids = List.map_filter Nameops.Name.to_option nal in
       Loc.tag @@ (ids,[p],c))
     brs
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bf62cea6b6..630f80ad2f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -638,7 +638,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
-               let na = Nameops.name_max na1 na2 in
+               let na = Nameops.Name.pick na1 na2 in
 	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
@@ -755,7 +755,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
 	     let c = nf_evar i c1 in
-             let na = Nameops.name_max na1 na2 in
+             let na = Nameops.Name.pick na1 na2 in
 	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -816,7 +816,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
               [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-                 let na = Nameops.name_max n1 n2 in
+                 let na = Nameops.Name.pick n1 n2 in
 	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 923d7d9388..faf44099cd 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -215,20 +215,20 @@ let fold_glob_constr f acc = CAst.with_val (function
   )
 
 let fold_return_type_with_binders f g v acc (na,tyopt) =
-  Option.fold_left (f (name_fold g na v)) acc tyopt
+  Option.fold_left (f (Name.fold_right g na v)) acc tyopt
 
 let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
   | GVar _ -> acc
   | GApp (c,args) -> List.fold_left (f v) (f v acc c) args
   | GLambda (na,_,b,c) | GProd (na,_,b,c) ->
-    f (name_fold g na v) (f v acc b) c
+    f (Name.fold_right g na v) (f v acc b) c
   | GLetIn (na,b,t,c) ->
-    f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c
+    f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c
   | GCases (_,rtntypopt,tml,pl) ->
     let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in
     let fold_tomatch (v',acc) (tm,(na,onal)) =
-      (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'')
-                        (name_fold g na v') onal,
+      (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'')
+                        (Name.fold_right g na v') onal,
        f v acc tm) in
     let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
     let acc = Option.fold_left (f v') acc rtntypopt in
@@ -242,7 +242,7 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
       let v,acc =
 	List.fold_left
 	  (fun (v,acc) (na,k,bbd,bty) ->
-            (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty))
+            (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
           (v,acc)
           bll.(i) in
       f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
@@ -371,12 +371,12 @@ let loc_of_glob_constr c = c.CAst.loc
 
 let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
 let test_id l id = if collide_id l id then raise Not_found
-let test_na l na = name_iter (test_id l) na
+let test_na l na = Name.iter (test_id l) na
 
 let update_subst na l =
   let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in
-  let l' = name_fold Id.List.remove_assoc na l in
-  name_fold
+  let l' = Name.fold_right Id.List.remove_assoc na l in
+  Name.fold_right
     (fun id _ ->
      if in_range id l' then
        let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 1c8ad0cddd..0818a55256 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -340,15 +340,15 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
   | GLambda (na,bk,c1,c2) ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | GProd (na,bk,c1,c2) ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | GLetIn (na,c1,t,c2) ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
@@ -411,7 +411,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
     | { CAst.v = PatVar na } ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       na
     | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.")
   in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f76555b047..60511d9138 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,8 +151,8 @@ let tag_var = tag Tag.variable
 
   let pr_univ l =
     match l with
-      | [_,x] -> pr_name x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")"
+      | [_,x] -> Name.print x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,7 +166,7 @@ let tag_var = tag Tag.variable
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (pr_name u)
+    | GType (Some (_, u)) -> tag_type (Name.print u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -191,7 +191,7 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> pr_name u
+        | Some (_,u) -> Name.print u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
@@ -224,7 +224,7 @@ let tag_var = tag Tag.variable
 
   let pr_lname = function
     | (loc,Name id) -> pr_lident (loc,id)
-    | lna -> pr_located pr_name lna
+    | lna -> pr_located Name.print lna
 
   let pr_or_var pr = function
     | ArgArg x -> pr x
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c328b6032b..6aa136b606 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -56,7 +56,7 @@ open Decl_kinds
 
   let pr_lname = function
     | (loc,Name id) -> pr_lident (loc,id)
-    | lna -> pr_located pr_name lna
+    | lna -> pr_located Name.print lna
 
   let pr_smart_global = Pputils.pr_or_by_notation pr_reference
 
@@ -1022,13 +1022,13 @@ open Decl_kinds
                   | n, { name = id; recarg_like = k;
                          notation_scope = s;
                          implicit_status = imp } :: tl ->
-                    spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+                    spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
                       print_arguments (Option.map pred n) tl
               in
               let rec print_implicits = function
                 | [] -> mt ()
                 | (name, impl) :: rest ->
-                   spc() ++ pr_br impl (pr_name name) ++ print_implicits rest
+                   spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
               in
               print_arguments nargs args ++
                 if not (List.is_empty more_implicits) then
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0f7da36133..2b21b3f9e8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -132,7 +132,7 @@ let print_impargs_list prefix l =
 let print_renames_list prefix l =
   if List.is_empty l then [] else
   [add_colon prefix ++ str "Arguments are renamed to " ++
-    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+    hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
 
 let need_expansion impl ref =
   let typ = Global.type_of_global_unsafe ref in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 33a86402ef..87b31849ee 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -433,7 +433,7 @@ let explain_no_such_bound_variable evd id =
     | Cltyp (na, _) -> na
     | Clval (na, _, _) -> na
     in
-    if na != Anonymous then out_name na :: l else l
+    if na != Anonymous then Name.get_id na :: l else l
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
   user_err ~hdr:"Evd.meta_with_name"
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e8cb4e632..85971e6650 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2975,7 +2975,7 @@ let specialize (c,lbind) ipat =
       if occur_meta clause.evd term then
 	user_err  (str "Cannot infer an instance for " ++
 
-          pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++
+          Name.print (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++
 	  str ".");
       clause.evd, term in
   let typ = Retyping.get_type_of env sigma term in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index cf534f13a2..b99ccbf4a2 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -533,7 +533,7 @@ open Namegen
 let compute_bl_goal ind lnamesparrec nparrec =
   let eqI, eff = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
   let create_input c =
     let x = next_ident_away (Id.of_string "x") avoid and
         y = next_ident_away (Id.of_string "y") avoid in
@@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
-  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
   let eqI, eff = eqI ind lnamesparrec in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
@@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
           y = next_ident_away (Id.of_string "y") avoid in
diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7fb..6ece585a9e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -411,8 +411,8 @@ let mk_mltype_data evdref env assums arity indname =
   (is_ml_type,indname,assums)
 
 let prepare_param = function
-  | LocalAssum (na,t) -> out_name na, LocalAssumEntry t
-  | LocalDef (na,b,_) -> out_name na, LocalDefEntry b
+  | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t
+  | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b
 
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
@@ -590,7 +590,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (RelDecl.get_name %> out_name) assums in
+  let params = List.map (RelDecl.get_name %> Name.get_id) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 17bb87f2aa..6d8dd82ac6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result =
 
 let explain_abstraction_over_meta _ m n =
   strbrk "Too complex unification problem: cannot find a solution for both " ++
-  pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+  Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."
 
 let explain_non_linear_unification env sigma m t =
   let t = EConstr.to_constr sigma t in
   strbrk "Cannot unambiguously instantiate " ++
-  pr_name m ++ str ":" ++
+  Name.print m ++ str ":" ++
   strbrk " which would require to abstract twice on " ++
   pr_lconstr_env env sigma t ++ str "."
 
@@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty =
 let explain_refiner_unresolved_bindings l =
   str "Unable to find an instance for the " ++
   str (String.plural (List.length l) "variable") ++ spc () ++
-  prlist_with_sep pr_comma pr_name l ++ str"."
+  prlist_with_sep pr_comma Name.print l ++ str"."
 
 let explain_refiner_cannot_apply t harg =
   str "In refiner, a term of type" ++ brk(1,1) ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c1d64cfe9..405d37927f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1003,12 +1003,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let err_extra_args names =
     user_err ~hdr:"vernac_declare_arguments"
                  (strbrk "Extra arguments: " ++
-                    prlist_with_sep pr_comma pr_name names ++ str ".")
+                    prlist_with_sep pr_comma Name.print names ++ str ".")
   in
   let err_missing_args names =
     user_err ~hdr:"vernac_declare_arguments"
                  (strbrk "The following arguments are not declared: " ++
-                    prlist_with_sep pr_comma pr_name names ++ str ".")
+                    prlist_with_sep pr_comma Name.print names ++ str ".")
   in
 
   let rec check_extra_args extra_args =
@@ -1093,14 +1093,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
        match !example_renaming with
        | None -> mt ()
        | Some (o,n) ->
-          str "Argument " ++ pr_name o ++
-            str " renamed to " ++ pr_name n ++ str ".");
+          str "Argument " ++ Name.print o ++
+            str " renamed to " ++ Name.print n ++ str ".");
 
   let duplicate_names =
     List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
   in
   if not (List.is_empty duplicate_names) then begin
-    let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in
+    let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in
     user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
   end;
 
@@ -1129,7 +1129,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
        anonymous argument implicit *)
     | Anonymous :: _, (name, _) :: _ ->
        user_err ~hdr:"vernac_declare_arguments"
-                    (strbrk"Argument "++ pr_name name ++ 
+                    (strbrk"Argument "++ Name.print name ++ 
                        strbrk " cannot be declared implicit.")
 
     | Name id :: inf_names, (name, impl) :: implicits ->