diff options
Diffstat (limited to 'tactics/term_dnet.ml')
-rw-r--r-- | tactics/term_dnet.ml | 12 |
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 |