diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-04 14:50:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-06 10:01:19 +0200 |
| commit | 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f (patch) | |
| tree | 4bb7a90d8474b038434b732fb24b9b9d69e937c3 /tactics/hints.mli | |
| parent | efce61af32ff1b09a21dcf88bca7d6609a0bfd27 (diff) | |
Fix bug #4354: interpret hints in the right env and sigma.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 687bc78c7..5a4fb7709 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -93,8 +93,8 @@ module Hint_db : arguments. *) val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list - val add_one : hint_entry -> t -> t - val add_list : (hint_entry) list -> t -> t + val add_one : env -> evar_map -> hint_entry -> t -> t + val add_list : env -> evar_map -> hint_entry list -> t -> t val remove_one : global_reference -> t -> t val remove_list : global_reference list -> t -> t val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit |