5 files changed, 27 insertions, 0 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ee8e1855d5..4eb8a79256 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -211,6 +211,7 @@ let cache_hintrewrite (_,(rbase,lrl)) =
   let base = try raw_find_base rbase with Not_found -> HintDN.empty in
   let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0
   in
+  let lrl = HintDN.refresh_metas lrl in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab
 
diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index bb71620c09..93334db73c 100644
--- a/tactics/dnet.ml
+++ b/tactics/dnet.ml
@@ -39,6 +39,7 @@ sig
   val inter : t -> t -> t
   val union : t -> t -> t
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+  val map_metas : (meta -> meta) -> t -> t
 end
 
 module Make =
@@ -288,4 +289,13 @@ struct
       | Node e -> Node (T.map (map sidset sterm) e) in
     Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m)
 
+  let rec map_metas f (Nodes (t, m)) : t =
+    let f_node = function
+      | Terminal (e, is) -> Terminal (T.map (map_metas f) e, is)
+      | Node e -> Node (T.map (map_metas f) e)
+    in
+    let m' = Mmap.fold (fun m s acc -> Mmap.add (f m) s acc) m Mmap.empty in
+    let t' = Tmap.fold (fun k n acc -> Tmap.add k (f_node n) acc) t Tmap.empty in
+    Nodes (t', m')
+
 end
diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 4bfa7263e9..52853d7021 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -113,6 +113,8 @@ sig
 
   (** apply a function on each identifier and node of terms in a dnet *)
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+
+  val map_metas : (meta -> meta) -> t -> t
 end
 
 module Make :
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e637b2e36d..e79fc6dc9a 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
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index a5c80cc00e..58f95ac6c9 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -80,6 +80,8 @@ sig
   val find_all : t -> ident list
 
   val map : (ident -> ident) -> t -> t
+
+  val refresh_metas : t -> t
 end
 
 module Make :