diff options
Diffstat (limited to 'pretyping/matching.mli')
| -rw-r--r-- | pretyping/matching.mli | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 5a789b442..32c2906b6 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -13,38 +13,37 @@ open Names open Term open Environ open Pattern +open Termops (*i*) (*s This modules implements pattern-matching on terms *) exception PatternMatchingFailure +val special_meta : metavariable + (* [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 *) -val matches : - constr_pattern -> constr -> (int * constr) list +val matches : constr_pattern -> constr -> patvar_map (* [is_matching pat c] just tells if [c] matches against [pat] *) -val is_matching : - constr_pattern -> constr -> bool +val is_matching : constr_pattern -> constr -> bool (* [matches_conv env sigma] matches up to conversion in environment [(env,sigma)] when constants in pattern are concerned; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) -val matches_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list +val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (* To skip to the next occurrence *) exception NextOccurrence of int (* Tries to match a subterm of [c] with [pat] *) -val sub_match : - int -> constr_pattern -> constr -> ((int * constr) list * constr) +val sub_match : int -> constr_pattern -> constr -> patvar_map * constr (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] up to conversion for constants in patterns *) |