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/dnet.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'tactics/dnet.ml')

diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index 61a35866..93334db7 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 =
@@ -121,7 +122,7 @@ struct
 	     Idset.union acc s2
 	 ) t Idset.empty)
 
-(*   (\* optimization hack: Not_found is catched in fold_pattern *\) *)
+(*   (\* optimization hack: Not_found is caught in fold_pattern *\) *)
 (*   let fast_inter s1 s2 = *)
 (*     if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *)
 (*     else Idset.inter s1 s2 *)
@@ -176,7 +177,7 @@ struct
     let is_empty : t -> bool = function 
       | None -> false
       | Some s -> S.is_empty s
-    (* optimization hack: Not_found is catched in fold_pattern *)
+    (* optimization hack: Not_found is caught in fold_pattern *)
     let fast_inter s1 s2 =
       if is_empty s1 || is_empty s2 then raise Not_found
       else let r = inter s1 s2 in 
@@ -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
-- 
cgit v1.2.3