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).

1 files changed, 17 insertions, 2 deletions

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