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.

2 files changed, 6 insertions, 0 deletions

diff --git a/lib/rtree.ml b/lib/rtree.ml
index efcb6aae14..504cc67a07 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -167,6 +167,10 @@ let rec inter cmp interlbl def n histo t t' =
 
 let inter cmp interlbl def t t' = inter cmp interlbl def 0 [] t t'
 
+(** Inclusion of rtrees. We may want a more efficient implementation. *)
+let incl cmp interlbl def t t' =
+  equal cmp t (inter cmp interlbl def t t')
+
 (** Tests if a given tree is infinite, i.e. has a branch of infinite length.
    This corresponds to a cycle when visiting the expanded tree.
    We use a specific comparison to detect already seen trees. *)
diff --git a/lib/rtree.mli b/lib/rtree.mli
index b86f543540..8319e795e1 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