diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 29a4f4608..6f5ee8ba5 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -72,6 +72,7 @@ val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds val pp_hints_path : hints_path -> Pp.std_ppcmds +val pp_hint_mode : hint_mode -> Pp.std_ppcmds module Hint_db : sig @@ -99,7 +100,8 @@ module Hint_db : 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 + val iter : (global_reference option -> + hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state @@ -128,7 +130,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * bool list + | HintsModeEntry of global_reference * hint_mode list | HintsExternEntry of int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr |