diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 0b9da27ab3..e061bd7648 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -134,18 +134,18 @@ module Hint_db : (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. Returns a [ModeMismatch] if there are declared modes and none matches. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode + val map_eauto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode (** All hints associated to the reference. Precondition: no evars should appear in the arguments, so no modes are checked. *) - val map_auto : evar_map -> secvars:Id.Pred.t -> + val map_auto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t - val remove_one : GlobRef.t -> t -> t - val remove_list : GlobRef.t list -> t -> t + val remove_one : Environ.env -> GlobRef.t -> t -> t + val remove_list : Environ.env -> GlobRef.t list -> t -> t val iter : (GlobRef.t option -> hint_mode array list -> FullHint.t list -> unit) -> t -> unit |