diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-28 20:34:44 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-07-22 18:05:00 -0400 |
| commit | dcd3ec87a3bf26fab2856af720bbea5b0209cae5 (patch) | |
| tree | c92cece474e78d76ab7b4f6e6c67cb190da9aadf /lib/rtree.mli | |
| parent | cc001c2b8d5ababee585cc43e07e0f9089b5d40e (diff) | |
Refine check_is_subterm.
Following Bruno's suggestion, we check if the tree expected for the recursive
argument is included in the one which is inferred. This check is probably
not necessary in the current state of affairs, but might become so after
further extensions of the guard condition.
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 b86f54354..8319e795e 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -68,6 +68,8 @@ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool val inter : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> 'a t +val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> bool + (** Iterators *) val map : ('a -> 'b) -> 'a t -> 'b t |