From 258c8502eafd3e078a5c7478a452432b5c046f71 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 19:59:28 +0100
Subject: Constr_matching API using EConstr.

---
 proofs/tacmach.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 148f9d6752..5e9c0ba8e6 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -106,8 +106,8 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls          = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls
 
-let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
-let pf_matches                  = pf_apply Constr_matching.matches_conv
+let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c)
+let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c)
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -232,7 +232,7 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t))
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
+  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t)
 
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
-- 
cgit v1.2.3