From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 tactics/term_dnet.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'tactics/term_dnet.ml')

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
-- 
cgit v1.2.3