diff options
| author | Pierre Letouzey | 2014-03-02 14:17:09 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-02 20:00:03 +0100 |
| commit | 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae (patch) | |
| tree | 7c2a4361b949c5f496bdee7d56ce9f8aaa878277 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c0875d756f..de73f7720d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,8 +102,8 @@ let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) -let pf_is_matching = pf_apply Matching.is_matching_conv -let pf_matches = pf_apply Matching.matches_conv +let pf_is_matching = pf_apply ConstrMatching.is_matching_conv +let pf_matches = pf_apply ConstrMatching.matches_conv (************************************) (* Tactics handling a list of goals *) |