diff options
Diffstat (limited to 'pretyping/matching.mli')
| -rw-r--r-- | pretyping/matching.mli | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 5ce18931d3..c9bf60ad28 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -60,27 +60,23 @@ val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) + a continuation that either returns the next matching subterm or raise PatternMatchingFailure *) -type 'a matching_result = +type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : 'a; - m_nxt : unit -> 'a matching_result } + m_ctx : constr } (** [match_subterm n pat c] returns the substitution and the context corresponding to the first **closed** subterm of [c] matching [pat], and - a continuation that looks for the next matching subterm. - It raises PatternMatchingFailure if no subterm matches the pattern *) -val match_subterm : constr_pattern -> constr -> constr matching_result + a continuation that looks for the next matching subterm. *) +val match_subterm : constr_pattern -> constr -> matching_result IStream.t (** [match_appsubterm pat c] returns the substitution and the context corresponding to the first **closed** subterm of [c] matching [pat], - considering application contexts as well. It also returns a - continuation that looks for the next matching subterm. - It raises PatternMatchingFailure if no subterm matches the pattern *) -val match_appsubterm : constr_pattern -> constr -> constr matching_result + considering application contexts as well. *) +val match_appsubterm : constr_pattern -> constr -> matching_result IStream.t (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) val match_subterm_gen : bool (** true = with app context *) -> - constr_pattern -> constr -> constr matching_result + constr_pattern -> constr -> matching_result IStream.t (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) |