diff options
| author | Maxime Dénès | 2013-12-26 15:52:50 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 17:34:57 -0400 |
| commit | 286abd141d415a621cc8ea98055d8dc744c8b752 (patch) | |
| tree | e3811f8c42d965af5870b412b0499cb0ff89c3cd /lib/rtree.mli | |
| parent | 9b272a861bc3263c69b699cd2ac40ab2606543fa (diff) | |
Refining match subterm and commutative cut rules. The parameters that are
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
Diffstat (limited to 'lib/rtree.mli')
| -rw-r--r-- | lib/rtree.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/rtree.mli b/lib/rtree.mli index c3ec3a0c51..b1cfc35bcc 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -66,6 +66,8 @@ val equiv : then by logical equivalence [Rtree.equiv eq eq] *) val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool +val inter : ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> 'a t + (** Iterators *) val map : ('a -> 'b) -> 'a t -> 'b t |