From 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 15:19:03 +0200
Subject: Remove dead code in the Hints API.

---
 tactics/hints.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 58fbf2fd66..9595fa2033 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -489,7 +489,6 @@ module Hint_db :
 sig
 type t
 val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
-val find : GlobRef.t -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_existential : evar_map -> secvars:Id.Pred.t ->
-- 
cgit v1.2.3