diff options
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 645684a86..237ec0db8 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -242,6 +242,10 @@ and try_sub_match nocc pat lc = | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in try_sub_match_rec nocc pat [] lc +let match_subterm nocc pat c = + try sub_match nocc pat c + with NextOccurrence _ -> raise PatternMatchingFailure + let is_matching pat n = try let _ = matches pat n in true with PatternMatchingFailure -> false |