2 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 656a90c704..4c6c5e6310 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -367,6 +367,8 @@ struct
     possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init
 
   let find_all dn = Idset.elements (TDnet.find_all dn)
+
+  let map f dn = TDnet.map f (fun x -> x) dn
 end
     
 module type S =
@@ -385,4 +387,5 @@ sig
   val search_head_concl : t -> constr -> result list
   val search_eq_concl : t -> constr -> constr -> result list
   val find_all : t -> ident list
+  val map : (ident -> ident) -> t -> t
 end
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index ccf9624814..f6c1b5b611 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -102,6 +102,8 @@ sig
 
   (* [find_all dn] returns all idents contained in dn *)
   val find_all : t -> ident list
+
+  val map : (ident -> ident) -> t -> t
 end
 
 module Make :