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.
---
 API/API.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 6227f17c65..9a671b43b3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4964,8 +4964,6 @@ sig
 
   val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
 
-  val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool
-
   val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list
 
   val pr_gls    : Goal.goal Evd.sigma -> Pp.t
-- 
cgit v1.2.3