PatternMatchingFailure is the exception raised when pattern matching fails

special_meta is the default name of the meta holding the surrounding context in subterm matching

bound_ident_map represents the result of matching binding identifiers of the pattern with the binding identifiers of the term matched

matches pat c matches c against pat and returns the resulting assignment of metavariables; it raises PatternMatchingFailure if not matchable; bindings are given in increasing order based on the numbers given in the pattern

matches_head pat c does the same as matches pat c but accepts pat to match an applicative prefix of c

extended_matches pat c also returns the names of bound variables in c that matches the bound variables in pat; if several bound variables or metavariables have the same name, the metavariable, or else the rightmost bound variable, takes precedence

is_matching pat c just tells if c matches against pat

is_matching_head pat c just tells if c or an applicative prefix of it matches against pat

The type of subterm matching results: a substitution + a context (whose hole is denoted here with special_meta)

match_subterm pat c returns the substitution and the context corresponding to each **closed** subterm of c matching pat, considering application contexts as well.

is_matching_appsubterm pat c tells if a subterm of c matches against pat taking partial subterms into consideration