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 ----- 1 file changed, 5 deletions(-) (limited to 'proofs/tacmach.ml') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca..cab8d7b52 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 -- cgit v1.2.3