diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 14:17:09 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 20:00:03 +0100 |
| commit | 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae (patch) | |
| tree | 7c2a4361b949c5f496bdee7d56ce9f8aaa878277 /tactics/tacticMatching.ml | |
| parent | 9130ea9cbc657cd7adf02830e40a89f6de3953f3 (diff) | |
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
There are currently two other clashs : Lexer and Errors, but for
the moment these ones haven't impacted my experiments with extraction
and compiler-libs, while this Matching issue had. And anyway the new
name is more descriptive, in the spirit of the recent TacticMatching.
Diffstat (limited to 'tactics/tacticMatching.ml')
| -rw-r--r-- | tactics/tacticMatching.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index e52a9011c..85108f8ed 100644 --- a/tactics/tacticMatching.ml +++ b/tactics/tacticMatching.ml @@ -19,7 +19,7 @@ open Tacexpr those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ; context : Term.constr Id.Map.t; terms : Term.constr Id.Map.t; lhs : 'a; @@ -33,9 +33,9 @@ type 'a t = { (** Some of the functions of {!Matching} return the substitution with a [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces substitution of the former type to the latter. *) -let adjust : Matching.bound_ident_map * Pattern.patvar_map -> - Matching.bound_ident_map * Pattern.extended_patvar_map = fun (l, lc) -> - (l, Id.Map.map (fun c -> [], c) lc) +let adjust : ConstrMatching.bound_ident_map * Pattern.patvar_map -> + ConstrMatching.bound_ident_map * Pattern.extended_patvar_map = + fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc) (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) @@ -240,19 +240,19 @@ module PatternMatching (E:StaticEnvironment) = struct | Term p -> begin try - put_subst (Matching.extended_matches p term) <*> + put_subst (ConstrMatching.extended_matches p term) <*> return lhs - with Matching.PatternMatchingFailure -> fail + with ConstrMatching.PatternMatchingFailure -> fail end | Subterm (with_app_context,id_ctxt,p) -> (* spiwack: this branch is easier in direct style, would need to be changed if the implementation of the monad changes. *) - IStream.map begin fun { Matching.m_sub ; m_ctx } -> + IStream.map begin fun { ConstrMatching.m_sub ; m_ctx } -> let subst = adjust m_sub in let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in let terms = empty_term_subst in { subst ; context ; terms ; lhs } - end (Matching.match_subterm_gen with_app_context p term) + end (ConstrMatching.match_subterm_gen with_app_context p term) (** [rule_match_term term rule] matches the term [term] with the |