diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-10 01:15:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 98703c8247fd86deab2d82a70c22d43797e4a548 (patch) | |
| tree | f4357abeaab6a7db53419c2ed9b3c923d7d67914 /tactics/hints.mli | |
| parent | 2194292dbe88674fd9a606bb22f28d332f670f77 (diff) | |
Extend Hint Mode to handle the no-head-evar case
Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
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 |