2 files changed, 126 insertions, 31 deletions
diff --git a/library/nameops.ml b/library/nameops.ml
index 098f5112f..b73bd7eb3 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 3a67b61a1..abfc09db8 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