From 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 2 Mar 2014 14:17:09 +0100
Subject: 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.
---
 proofs/tacmach.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

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 *)
-- 
cgit v1.2.3