diff options
| -rw-r--r-- | tactics/hints.ml | 1 | ||||
| -rw-r--r-- | tactics/hints.mli | 3 |
2 files changed, 0 insertions, 4 deletions
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 -> diff --git a/tactics/hints.mli b/tactics/hints.mli index d8881c3b49..56bd6fad44 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -70,8 +70,6 @@ type 'a with_metadata = private type full_hint = hint with_metadata -type search_entry - (** The head may not be bound. *) type hint_entry @@ -117,7 +115,6 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t - val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. * [secvars] represent the set of section variables that |