1 files changed, 12 insertions, 0 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e637b2e3..e79fc6dc 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -371,6 +371,17 @@ struct
   let find_all dn = Idset.elements (TDnet.find_all dn)
 
   let map f dn = TDnet.map f (fun x -> x) dn
+
+  let refresh_metas dn =
+    let new_metas = ref Int.Map.empty in
+    let refresh_one_meta i =
+      try Int.Map.find i !new_metas
+      with Not_found ->
+        let new_meta = fresh_meta () in
+        let () = new_metas := Int.Map.add i new_meta !new_metas in
+        new_meta
+    in
+    TDnet.map_metas refresh_one_meta dn
 end
 
 module type S =
@@ -385,4 +396,5 @@ sig
   val search_pattern : t -> constr -> ident list
   val find_all : t -> ident list
   val map : (ident -> ident) -> t -> t
+  val refresh_metas : t -> t
 end