From 62a552b508b747b6cdf4bd818233f001ae4ce555 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 15 Sep 2014 21:33:48 +0200 Subject: Add a "Hint Mode ref (+ | -)*" hint for setting a global mode of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases). --- tactics/auto.mli | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'tactics/auto.mli') diff --git a/tactics/auto.mli b/tactics/auto.mli index 3c916af73..5fde1d2de 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -73,13 +73,27 @@ module Hint_db : val empty : transparent_state -> bool -> t val find : global_reference -> t -> search_entry val map_none : t -> pri_auto_tactic list + + (** All hints associated to the reference *) val map_all : global_reference -> t -> pri_auto_tactic list - val map_auto : global_reference * constr -> t -> pri_auto_tactic list + + (** All hints associated to the reference, respecting modes if evars appear in the + arguments, _not_ using the discrimination net. *) + val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + + (** All hints associated to the reference, respecting modes if evars appear in the + arguments and using the discrimination net. *) + val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + + (** All hints associated to the reference, respecting modes if evars appear in the + arguments. *) + val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val add_one : hint_entry -> t -> t val add_list : (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 -> pri_auto_tactic list -> unit) -> t -> unit + val iter : (global_reference option -> bool array list -> pri_auto_tactic list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state @@ -108,6 +122,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 | HintsExternEntry of int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr -- cgit v1.2.3