Tentative patch for incompatibility between subterm relation and dependent

pattern matching.

This patch should be improved in two ways:
(1) Implement the same checks for the commutative cut subterm rule.
(2) When checking safe recursive subterms for each of the branches in a match,
instanciated parameters in the return predicate should be taken into account.

Step (1) should be enough to restore a correct guard condition, but (2) will
be required if we don't want to rule out some legitimate and practical examples.

0 files changed, 0 insertions, 0 deletions