From 59cd53f187939ad32c268cc8ec995d58cee4c297 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Dec 2017 11:10:43 +0100
Subject: Remove up-to-conversion matching functions.

They were not used anymore since the previous patches.
---
 proofs/tacmach.ml  | 5 -----
 proofs/tacmach.mli | 8 --------
 2 files changed, 13 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a8ec4d8ca3..cab8d7b52a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
-let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
-let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
-
 (********************************************)
 (* Definition of the most primitive tactics *)
 (********************************************)
@@ -223,8 +220,6 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
-
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d9496d2b4f..e0fb8fbc5d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -12,9 +12,7 @@ open Environ
 open EConstr
 open Proof_type
 open Redexpr
-open Pattern
 open Locus
-open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
@@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-
-
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
@@ -138,8 +132,6 @@ module New : sig
   val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
   val pf_compute : 'a Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
-
   val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
 
 end
-- 
cgit v1.2.3