diff options
| author | Pierre-Marie Pédrot | 2020-06-08 15:19:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 (patch) | |
| tree | 58f5d80f47dd35f68dbb1fb8d1e0d9ab5783df46 /tactics/hints.ml | |
| parent | 7ac18ed989a884e9d44917c916c7aae016582fe4 (diff) | |
Remove dead code in the Hints API.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 1 |
1 files changed, 0 insertions, 1 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 -> |