diff options
Diffstat (limited to 'lib/rtree.ml')
| -rw-r--r-- | lib/rtree.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml index 8f859b47e..b7fe9184e 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -101,7 +101,7 @@ let rec map f t = match t with | Node (a,sons) -> Node (f a, Array.map (map f) sons) | Rec(j,defs) -> Rec (j, Array.map (map f) defs) -let rec smartmap f t = match t with +let smartmap f t = match t with Param _ -> t | Node (a,sons) -> let a'=f a and sons' = Util.array_smartmap (map f) sons in |