From 98703c8247fd86deab2d82a70c22d43797e4a548 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 10 Jun 2016 01:15:38 +0200 Subject: 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. --- tactics/hints.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'tactics/hints.mli') 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 -- cgit v1.2.3