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

13 files changed, 198 insertions, 82 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 009ec543c..e670f68c2 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -125,6 +125,7 @@ type hints_expr =
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
+  | HintsMode of reference * bool list
   | HintsConstructors of reference list
   | HintsExtern of int * constr_expr option * raw_tactic_expr
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 212d4af6d..2c8eb85b8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -146,6 +146,7 @@ GEXTEND Gram
       | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
       | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
       | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
+      | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m)
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
       | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
@@ -156,4 +157,7 @@ GEXTEND Gram
     [ [ ":="; c = lconstr -> c
       | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ]
   ;
+  mode:
+    [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ]
+  ;
 END
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index afa178832..6d4d8792f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -218,7 +218,7 @@ let extend_with_auto_hints l seq gl=
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
-  let g _ l = List.iter f l in
+  let g _ _ l = List.iter f l in
   let h dbname=
     let hdb=
       try
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 420666356..5828e7f43 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -157,7 +157,7 @@ let pattern_of_constr sigma t =
           | Evar_kinds.MatchingVar (b,id) ->
               ctx := (id,None,existential_type sigma ev)::!ctx;
               assert (not b); PMeta (Some id)
-          | Evar_kinds.GoalEvar _ -> PEvar (evk,Array.map pattern_of_constr ctxt)
+          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b7ac274b7..a075265cc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -172,6 +172,9 @@ let pr_hints db h pr_c pr_pat =
     | HintsTransparency (l, b) ->
         str (if b then "Transparent " else "Opaque ") ++ prlist_with_sep sep
 	  pr_reference l
+    | HintsMode (m, l) ->
+        str "Mode " ++ pr_reference m ++ spc() ++ prlist_with_sep spc 
+	  (fun b -> if b then str"+" else str"-") l
     | HintsConstructors c ->
         str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
     | HintsExtern (n,c,tac) ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e386728fe..0f1d7cb02 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -137,9 +137,10 @@ module Bounded_net = Btermdn.Make(struct
 				    let compare = pri_order_int
 				  end)
 
-type search_entry = stored_data list * stored_data list * Bounded_net.t
+type search_entry = stored_data list * stored_data list * Bounded_net.t * bool array list
 
-let empty_se = ([],[],Bounded_net.create ())
+
+let empty_se = ([],[],Bounded_net.create (),[])
 
 let eq_pri_auto_tactic (_, x) (_, y) =
   if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
@@ -157,20 +158,25 @@ let eq_pri_auto_tactic (_, x) (_, y) =
   else
     false
 
-let add_tac pat t st (l,l',dn) =
+let add_tac pat t st (l,l',dn,m) =
   match pat with
-  | None -> if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn) else (l, l', dn)
+  | None -> 
+    if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn, m) 
+    else (l, l', dn, m)
   | Some pat -> 
-    if not (List.exists (eq_pri_auto_tactic t) l') 
-    then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
-
-let rebuild_dn st ((l,l',dn) : search_entry) =
-  (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
-    (Bounded_net.create ()) l')
-
+    if not (List.exists (eq_pri_auto_tactic t) l')
+    then (l, insert t l', Bounded_net.add st dn (pat,t), m) else (l, l', dn, m)
+
+let rebuild_dn st ((l,l',dn,m) : search_entry) =
+  let dn' = 
+    List.fold_left 
+      (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
+      (Bounded_net.create ()) l'
+  in
+    (l, l', dn', m)
 
-let lookup_tacs (hdc,c) st (l,l',dn) =
-  let l'  = Bounded_net.lookup st dn c in
+let lookup_tacs concl st (l,l',dn) =
+  let l'  = Bounded_net.lookup st dn concl in
   let sl' = List.stable_sort pri_order_int l' in
     List.merge pri_order_int l sl'
 
@@ -378,18 +384,43 @@ module Hint_db = struct
  
   let realize_tac (id,tac) = tac
 
+  let matches_mode args mode =
+    Array.length args == Array.length mode &&
+      Array.for_all2 (fun arg m -> not (m && occur_existential arg)) args mode
+      
+  let matches_modes args modes =
+    if List.is_empty modes then true
+    else List.exists (matches_mode args) modes
+
   let map_none db =
     List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
     
   let map_all k db =
-    let (l,l',_) = find k db in
+    let (l,l',_,_) = find k db in
       List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
-
-  let map_auto (k,c) db =
-    let st = if db.use_dn then Some db.hintdb_state else None in
-    let l' = lookup_tacs (k,c) st (find k db) in
+	
+  (** Precondition: concl has no existentials *)
+  let map_auto (k,args) concl db =
+    let (l,l',dn,m) = find k db in
+    let st = if db.use_dn then  (Some db.hintdb_state) else None in
+    let l' = lookup_tacs concl st (l,l',dn) in
       List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
 
+  let map_existential (k,args) concl db =
+    let (l,l',_,m) = find k db in
+      if matches_modes args m then
+	List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
+      else List.map realize_tac (List.map snd db.hintdb_nopat)
+
+  (* [c] contains an existential *)
+  let map_eauto (k,args) concl db =
+    let (l,l',dn,m) = find k db in
+      if matches_modes args m then
+	let st = if db.use_dn then Some db.hintdb_state else None in
+	let l' = lookup_tacs concl st (l,l',dn) in
+	  List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
+      else List.map realize_tac (List.map snd db.hintdb_nopat)
+
   let is_exact = function
     | Give_exact _ -> true
     | _ -> false
@@ -446,10 +477,10 @@ module Hint_db = struct
   let add_list l db = List.fold_left (fun db k -> add_one k db) db l
 
   let remove_sdl p sdl = List.smartfilter p sdl 
-  let remove_he st p (sl1, sl2, dn as he) =
+  let remove_he st p (sl1, sl2, dn, m as he) =
     let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
       if sl1' == sl1 && sl2' == sl2 then he
-      else rebuild_dn st (sl1', sl2', dn)
+      else rebuild_dn st (sl1', sl2', dn, m)
 
   let remove_list grs db =
     let filter (_, h) =
@@ -461,12 +492,12 @@ module Hint_db = struct
   let remove_one gr db = remove_list [gr] db
 
   let iter f db =
-    f None (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
-    Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map realize_tac (l@l'))) db.hintdb_map
+    f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
+    Constr_map.iter (fun k (l,l',_,m) -> f (Some k) m (List.map realize_tac (l@l'))) db.hintdb_map
 
   let fold f db accu =
-    let accu = f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
-    Constr_map.fold (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map accu
+    let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
+    Constr_map.fold (fun k (l,l',_,m) -> f (Some k) m (List.map snd (l@l'))) db.hintdb_map accu
 
   let transparent_state db = db.hintdb_state
 
@@ -477,6 +508,10 @@ module Hint_db = struct
   let add_cut path db =
     { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
 
+  let add_mode gr m db =
+    let (l,l',dn,ms) = find gr db in
+      { db with hintdb_map = Constr_map.add gr (l,l',dn,m :: ms) db.hintdb_map }
+
   let cut db = db.hintdb_cut
 
   let unfolds db = db.hintdb_unfolds
@@ -648,6 +683,17 @@ let make_extern pri pat tacast =
      name = PathAny;
      code = Extern tacast })  
 
+let make_mode ref m = 
+  let ty = Global.type_of_global_unsafe ref in
+  let ctx, t = decompose_prod ty in
+  let n = List.length ctx in
+  let m' = Array.of_list m in
+    if not (n == Array.length m') then
+      errorlabstrm "Hint"
+	(pr_global ref ++ str" has " ++ int n ++ 
+	   str" arguments while the mode declares " ++ int (Array.length m'))
+    else m'
+      
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let t = hnf_constr env sigma (type_of env sigma c) in
@@ -699,12 +745,18 @@ type hint_action =
   | AddHints of hint_entry list
   | RemoveHints of global_reference list
   | AddCut of hints_path
+  | AddMode of global_reference * bool array
 
 let add_cut dbname path =
   let db = get_db dbname in
   let db' = Hint_db.add_cut path db in
     searchtable_add (dbname, db')
 
+let add_mode dbname l m =
+  let db = get_db dbname in
+  let db' = Hint_db.add_mode l m db in
+    searchtable_add (dbname, db')
+
 type hint_obj = bool * string * hint_action  (* locality, name, action *)
 
 let cache_autohint (_,(local,name,hints)) =
@@ -714,19 +766,10 @@ let cache_autohint (_,(local,name,hints)) =
   | AddHints hints -> add_hint name hints
   | RemoveHints grs -> remove_hint name grs
   | AddCut path -> add_cut name path
+  | AddMode (l, m) -> add_mode name l m
 
 let (forward_subst_tactic, extern_subst_tactic) = Hook.make ()
 
-  (* let subst_mps_or_ref subst cr =  *)
-  (*   match cr with *)
-  (*   | IsConstr c -> let c' = subst_mps subst c in  *)
-  (* 		      if c' == c then cr *)
-  (* 		      else IsConstr c' *)
-  (*   | IsGlobal r -> let r' = subst_global_reference subst r in *)
-  (* 			 if r' == r then cr *)
-  (* 			 else IsGlobal r' *)
-  (* in *)
-
 let subst_autohint (subst,(local,name,hintlist as obj)) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
@@ -779,11 +822,14 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
 	  if hintlist' == hintlist then obj else
 	    (local,name,AddHints hintlist')
     | RemoveHints grs ->
-	let grs' = List.smartmap (fun x -> fst (subst_global subst x)) grs in
+	let grs' = List.smartmap (subst_global_reference subst) grs in
 	  if grs==grs' then obj else (local, name, RemoveHints grs')
     | AddCut path ->
       let path' = subst_hints_path subst path in
 	if path' == path then obj else (local, name, AddCut path')
+    | AddMode (l,m) ->
+      let l' = subst_global_reference subst l in
+	(local, name, AddMode (l', m))
 
 let classify_autohint ((local,name,hintlist) as obj) =
   match hintlist with
@@ -835,6 +881,13 @@ let add_cuts l local dbnames =
        (inAutoHint (local,dbname, AddCut l)))
     dbnames
 
+let add_mode l m local dbnames =
+  List.iter
+    (fun dbname -> Lib.add_anonymous_leaf
+      (let m' = make_mode l m in
+	 (inAutoHint (local,dbname, AddMode (l,m')))))
+    dbnames
+
 let add_transparency l b local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
@@ -870,6 +923,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 * glob_tactic_expr
 
@@ -914,22 +968,19 @@ let interp_hints poly =
   let f c =
     let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in
       prepare_hint true (Global.env()) Evd.empty (evd,c) in
-  let fr r =
+  let fref r =
     let gr = global_with_alias r in
-    let r' = evaluable_of_global_reference (Global.env()) gr in
     Dumpglob.add_glob (loc_of_reference r) gr;
-    r' in
+    gr in
+  let fr r = 
+    evaluable_of_global_reference (Global.env()) (fref r)
+  in
   let fi c =
     match c with
     | HintsReference c ->
       let gr = global_with_alias c in
 	(PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c -> 
-      (* if poly then *)
-      (* 	errorlabstrm "Hint" (Ppconstr.pr_constr_expr c ++ spc () ++  *)
-      (* 			     str" is a term and cannot be made a polymorphic hint," ++ *)
-      (* 			     str" only global references can be polymorphic hints.") *)
-      (* else *) (PathAny, poly, f c)
+    | HintsConstr c -> (PathAny, poly, f c)
   in
   let fres (pri, b, r) =
     let path, poly, gr = fi r in
@@ -942,6 +993,7 @@ let interp_hints poly =
   | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
   | HintsTransparency (lhints, b) ->
       HintsTransparencyEntry (List.map fr lhints, b)
+  | HintsMode (r, l) -> HintsModeEntry (fref r, l)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
@@ -968,6 +1020,7 @@ let add_hints local dbnames0 h =
   | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
   | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
   | HintsCutEntry lhints -> add_cuts lhints local dbnames
+  | HintsModeEntry (l,m) -> add_mode l m local dbnames
   | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b local dbnames
@@ -1030,11 +1083,10 @@ let pr_hint_term cl =
     let dbs = current_db () in
     let valid_dbs =
       let fn = try
-	  let hdc = head_constr_bound cl in
-	  let hd = head_of_constr_reference hdc in
+	  let hdc = decompose_app_bound cl in
 	    if occur_existential cl then
-	      Hint_db.map_all hd
-	    else Hint_db.map_auto (hd, cl)
+	      Hint_db.map_existential hdc cl
+	    else Hint_db.map_auto hdc cl
 	with Bound -> Hint_db.map_none
       in
       let fn db = List.map (fun x -> 0, x) (fn db) in
@@ -1063,11 +1115,16 @@ let pr_applicable_hint () =
 
 (* displays the whole hint database db *)
 let pr_hint_db db =
+  let pr_mode = prvect_with_sep spc (fun x -> if x then str"+" else str"-") in
+  let pr_modes l = 
+    if List.is_empty l then mt ()
+    else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")"
+  in
   let content =
-    let fold head hintlist accu =
+    let fold head modes hintlist accu =
       let goal_descr = match head with
       | None -> str "For any goal"
-      | Some head -> str "For " ++ pr_global head
+      | Some head -> str "For " ++ pr_global head ++ pr_modes modes
       in
       let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
       let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
@@ -1395,8 +1452,8 @@ let hintmap_of hdc concl =
   match hdc with
   | None -> Hint_db.map_none
   | Some hdc ->
-      if occur_existential concl then Hint_db.map_all hdc
-      else Hint_db.map_auto (hdc,concl)
+      if occur_existential concl then Hint_db.map_existential hdc concl
+      else Hint_db.map_auto hdc concl
 
 let exists_evaluable_reference env = function
   | EvalConstRef _ -> true
@@ -1458,8 +1515,8 @@ and my_find_search_delta db_list local_db hdc concl =
 	      match hdc with None -> Hint_db.map_none db
 	      | Some hdc ->
 		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
-		  then Hint_db.map_auto (hdc,concl) db
-		  else Hint_db.map_all hdc db
+		  then Hint_db.map_auto hdc concl db
+		  else Hint_db.map_existential hdc concl db
 	    in auto_flags_of_state st, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
@@ -1489,8 +1546,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
     let head =
-      try let hdconstr = head_constr_bound cl in
-	    Some (head_of_constr_reference hdconstr)
+      try let hdconstr = decompose_app_bound cl in
+	    Some hdconstr
       with Bound -> None
     in
       List.map (tac_of_hint dbg db_list local_db cl)
@@ -1543,8 +1600,8 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
 let possible_resolve dbg mod_delta db_list local_db cl =
   try
     let head =
-      try let hdconstr = head_constr_bound cl in
-	    Some (head_of_constr_reference hdconstr)
+      try let hdconstr = decompose_app_bound cl in
+	    Some hdconstr
       with Bound -> None
     in
       List.map (tac_of_hint dbg db_list local_db cl)
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
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 77101c70e..7de9330ba 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -151,12 +151,11 @@ let rec e_trivial_fail_db db_list local_db goal =
   tclFIRST (List.map tclCOMPLETE tacl) goal
 
 and e_my_find_search db_list local_db hdc complete sigma concl =
-  let hdc = head_of_constr_reference hdc in
   let prods, concl = decompose_prod_assum concl in
   let nprods = List.length prods in
   let freeze = 
     try
-      let cl = Typeclasses.class_info hdc in
+      let cl = Typeclasses.class_info (fst hdc) in
 	if cl.cl_strict then
 	  Evarutil.evars_of_term concl
 	else Evar.Set.empty
@@ -165,12 +164,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   let hintl =
     List.map_append
       (fun db ->
-	if Hint_db.use_dn db then
-	  let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
-	    List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
-	else
-	  let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
-	    List.map (fun x -> (flags, x)) (Hint_db.map_all hdc db))
+	let tacs = 
+	  if Hint_db.use_dn db then (* Using dnet *)
+	    Hint_db.map_eauto hdc concl db
+	  else Hint_db.map_existential hdc concl db
+	in
+	let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
+	  List.map (fun x -> (flags, x)) tacs)
       (local_db::db_list)
   in
   let tac_of_hint =
@@ -198,13 +198,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
 and e_trivial_resolve db_list local_db sigma concl =
   try
     e_my_find_search db_list local_db
-     (head_constr_bound concl) true sigma concl
+     (decompose_app_bound concl) true sigma concl
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db sigma concl =
   try
     e_my_find_search db_list local_db
-      (head_constr_bound concl) false sigma concl
+      (decompose_app_bound concl) false sigma concl
   with Bound | Not_found -> []
 
 let catchable = function
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5676a3b58..7a4639967 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -141,19 +141,19 @@ let rec e_trivial_fail_db db_list local_db goal =
 	      (Hint_db.add_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in
-  tclFIRST (List.map tclCOMPLETE tacl) goal
+    tclFIRST (List.map tclCOMPLETE tacl) goal
 
 and e_my_find_search db_list local_db hdc concl =
-  let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
+	  List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db)
+   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list)
     else
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+	  List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list)
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
@@ -177,13 +177,13 @@ and e_trivial_resolve db_list local_db gl =
   try
     priority
       (e_my_find_search db_list local_db
-	 (head_constr_bound gl) gl)
+	 (decompose_app_bound gl) gl)
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
   try List.map snd
     (e_my_find_search db_list local_db
-	(head_constr_bound gl) gl)
+	(decompose_app_bound gl) gl)
   with Bound | Not_found -> []
 
 let find_first_goal gls =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 48bfeb86e..36a297c81 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -130,6 +130,18 @@ let head_constr_bound t =
 let head_constr c =
   try head_constr_bound c with Bound -> error "Bound head variable."
 
+let decompose_app_bound t =
+  let t = strip_outer_cast t in
+  let _,ccl = decompose_prod_assum t in
+  let hd,args = decompose_app_vect ccl in
+  match kind_of_term hd with
+    | Const (c,u) -> ConstRef c, args
+    | Ind (i,u) -> IndRef i, args
+    | Construct (c,u) -> ConstructRef c, args
+    | Var id -> VarRef id, args
+    | Proj (p, c) -> ConstRef p, Array.cons c args
+    | _ -> raise Bound
+
 (******************************************)
 (*           Primitive tactics            *)
 (******************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d6e648b9b..c076efb1f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,12 +26,13 @@ open Locus
 
 (** {6 General functions. } *)
 
+exception Bound
+
 val head_constr       : constr -> constr
 val head_constr_bound : constr -> constr
+val decompose_app_bound : constr -> global_reference * constr array
 val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 
-exception Bound
-
 (** {6 Primitive tactics. } *)
 
 val introduction    : Id.t -> tactic
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index fb9f8c218..db3b19af5 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -24,3 +24,24 @@ auto using (pair O).
 Undo.
 eauto using (pair O).
 Qed.
+
+Create HintDb test discriminated.
+
+Parameter foo : forall x, x = x + 0.
+Hint Resolve foo : test.
+
+Variable C : nat -> Type -> Prop.
+
+Variable c_inst : C 0 nat.
+
+Hint Resolve c_inst : test.
+
+Hint Mode C - + : test.
+Hint Resolve c_inst : test2.
+Hint Mode C + + : test2.
+
+Goal exists n, C n nat.
+Proof.
+  eexists. Fail progress debug eauto with test2. 
+  progress eauto with test.
+Qed.
diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v
index 112112f0c..fff740edd 100644
--- a/test-suite/typeclasses/backtrack.v
+++ b/test-suite/typeclasses/backtrack.v
@@ -1,5 +1,3 @@
-Set Typeclasses Strict Resolution.
-
 (* Set Typeclasses Unique Instances *)
 (** This lets typeclass search assume that instance heads are unique,
     so if one matches no other need to be tried,
@@ -14,6 +12,10 @@ Set Typeclasses Unique Instances.
 (* Unique *)
 Class D.
 Class C (A : Type) := c : A.
+
+Hint Mode C +.
+Fail Definition test := c.
+
 Unset Typeclasses Unique Instances.
 Instance : B -> D -> C nat := fun _ _ => 0.
 Instance : A -> D -> C nat := fun _ _ => 0.