Change implementation of resolution for typeclasses to use a customized

eauto instead of an arbitrary tactic. Export more from eauto to allow
easier debugging.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 342 insertions, 207 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index cf9c90e17e..f605988440 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -86,12 +86,12 @@ let type_class_instance_params isevars env id n ctx inst subst =
     (fun (subst, instctx) (na, _, t) ce ->
       let t' = replace_vars subst t in
       let c = 
-	if ce = superclass_ce then
-	  (* Control over the evars which are direct superclasses to avoid partial instanciations
-	     in instance search. *)
-	  Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t'
-	else
-	  interp_casted_constr_evars isevars env ce t' 
+(* 	if ce = superclass_ce then *)
+	(* 	  (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
+	(* 	     in instance search. *\) *)
+	(* 	  Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
+	(* 	else *)
+	interp_casted_constr_evars isevars env ce t' 
       in
       let d = na, Some c, t' in
 	(na, c) :: subst, d :: instctx)
@@ -154,7 +154,7 @@ let new_instance ctx (instid, bk, cl) props =
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses env' sigma !isevars;
+  isevars := resolve_typeclasses ~onlyargs:false ~all:true env' sigma !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index aba11231cd..84d374028b 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -72,8 +72,8 @@ let interp env isevars c tycon =
   let j = pretype tycon env isevars ([],[]) c in
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
-  let unevd = undefined_evars evd in
-  let unevd' = Typeclasses.resolve_typeclasses env (Evd.evars_of unevd) evd in
+(*   let unevd = undefined_evars evd in *)
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (Evd.evars_of evd) evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index a59d2483e2..5bcbf4db6c 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -573,7 +573,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
     let evd = nf_evar_defs evd in
-    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
     let c' = nf_evar (evars_of evd) c' in
       isevars := evd;
       c'
@@ -617,7 +617,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
 
   let understand_type sigma env c =
-    snd (ise_pretype_gen true sigma env ([],[]) IsType c)
+    snd (ise_pretype_gen false sigma env ([],[]) IsType c)
 
   let understand_ltac sigma env lvar kind c =
     ise_pretype_gen false sigma env lvar kind c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e30f553fe0..3992648592 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -362,7 +362,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      (* If recursive argument was not given by user, we try all args.
 	         An earlier approach was to look only for inductive arguments,
 		 but doing it properly involves delta-reduction, and it finally 
-                 doesn't seem to worth the effort (except for huge mutual 
+                 doesn't seem worth the effort (except for huge mutual 
 		 fixpoints ?) *)
 	      let possible_indexes = Array.to_list (Array.mapi 
 		(fun i (n,_) -> match n with 
@@ -668,8 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let evd = nf_evar_defs evd in
-    let c' = nf_evar (evars_of evd) c' in
-    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
     let c' = nf_evar (evars_of evd) c' in
       evdref := evd;
       c'
@@ -684,7 +683,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
-    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:true env (evars_of evd) evd in
     let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f9ab283ada..7a95f9c35e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -216,7 +216,7 @@ let instances r =
     with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
-let solve_instanciations_problem = ref (fun _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -278,34 +278,43 @@ let destClassApp c =
     | _ when isInd c -> Some (destInd c, [||])
     | _ -> None
 
-let resolve_typeclasses ?(check=true) env sigma evd =
+let is_independent evm ev = 
+  Evd.fold (fun ev' evi indep -> indep && 
+    (ev = ev' || 
+	evi.evar_body <> Evar_empty ||
+	not (Termops.occur_evar ev evi.evar_concl)))
+    evm true
+    
+
 (*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
 (*   with _ -> *)
-  let evm = Evd.evars_of evd in
-  let tc_evars = 
-    let f ev evi acc =
-      let (l, k) = Evd.evar_source ev evd in
-	if not check || is_implicit_arg k then
-	  match destClassApp evi.evar_concl with
-	    | Some (i, args) when is_class i -> 
-		Evd.add acc ev evi
-	    | _ -> acc
-	else acc
-    in Evd.fold f evm Evd.empty
-  in
-  let rec sat evars =
-    let (evars', progress) = 
-      Evd.fold 
-	(fun ev evi acc -> 
-	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
-	    resolve_typeclass env ev evi acc 
-	  else acc)
-	(Evd.evars_of evars) (evars, false) 
-    in
-      if not progress then evars'
-      else
-	sat (Evarutil.nf_evar_defs evars')
-  in sat (Evarutil.nf_evar_defs evd)
+(*   let evm = Evd.evars_of evd in *)
+(*   let tc_evars =  *)
+(*     let f ev evi acc = *)
+(*       let (l, k) = Evd.evar_source ev evd in *)
+(* 	if not check || is_implicit_arg k then *)
+(* 	  match destClassApp evi.evar_concl with *)
+(* 	    | Some (i, args) when is_class i ->  *)
+(* 		Evd.add acc ev evi *)
+(* 	    | _ -> acc *)
+(* 	else acc *)
+(*     in Evd.fold f evm Evd.empty *)
+(*   in *)
+(*   let rec sat evars = *)
+(*     let evm = Evd.evars_of evars in *)
+(*     let (evars', progress) =  *)
+(*       Evd.fold  *)
+(* 	(fun ev evi acc ->  *)
+(* 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev))  *)
+(* 	    && evi.evar_body = Evar_empty then *)
+(* 	    resolve_typeclass env ev evi acc  *)
+(* 	  else acc) *)
+(* 	evm (evars, false)  *)
+(*     in *)
+(*       if not progress then evars' *)
+(*       else *)
+(* 	sat (Evarutil.nf_evar_defs evars') *)
+(*   in sat (Evarutil.nf_evar_defs evd) *)
   
 let class_of_constr c = 
   let extract_ind c =
@@ -317,6 +326,16 @@ let class_of_constr c =
 	App (c, _) -> extract_ind c
       | _ -> extract_ind c
 
+let has_typeclasses evd =
+  Evd.fold (fun ev evi has -> has || 
+    (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None))
+    evd false
+
+let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd =
+  if not (has_typeclasses sigma) then evd
+  else
+    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs all
+
 type substitution = (identifier * constr) list
 
 let substitution_of_named_context isevars env id n subst l = 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index db408c8898..f231c7406d 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -61,10 +61,10 @@ val is_class : inductive -> bool
 val class_of_constr : constr -> typeclass option
 
 val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
-val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
-val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref
+val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref
 
 type substitution = (identifier * constr) list
 
@@ -73,3 +73,5 @@ val substitution_of_named_context :
   substitution -> named_context -> substitution
 
 val nf_substitution : evar_map -> substitution -> substitution
+
+val is_implicit_arg : hole_kind -> bool
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index b0a6b36c6d..84c1937ea8 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -99,14 +99,6 @@ let morphism_class = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
 exception Found of (constr * constr * (types * types) list * constr * constr array *
 		       (constr * (constr * constr * constr * constr)) option array)
 
-let resolve_morphism_evd env evd app = 
-  let ev = Evarutil.e_new_evar evd env app in
-  let evd' = resolve_typeclasses ~check:true env (Evd.evars_of !evd) !evd in
-  let evm' = Evd.evars_of evd' in
-    match Evd.evar_body (Evd.find evm' (fst (destEvar ev))) with
-	Evd.Evar_empty -> raise Not_found
-      | Evd.Evar_defined c -> evd := Evarutil.nf_evar_defs evd'; Evarutil.nf_isevar !evd c
-
 let is_equiv env sigma t = 
   isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t
 
@@ -139,7 +131,6 @@ let build_signature isevars env m cstrs finalcstr =
 		let rel = mk_relty t None in 
 		  rel, [t, rel]
 	    | Some (t, rel) -> rel, [t, rel])
-      | _, _ -> assert false
   in aux m cstrs
 
 let reflexivity_proof env evars carrier relation x =
@@ -174,31 +165,19 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
 	done;
 	!first
     in
-(*       try  *)
-	let morphargs, morphobjs = array_chop first args in
-	let morphargs', morphobjs' = array_chop first args' in
-	let appm = mkApp(m, morphargs) in
-	let appmtype = Typing.type_of env sigma appm in
-	let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
-	let cl_args = [| appmtype ; signature ; appm |] in
-	let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
-(* 	let morph = resolve_morphism_evd env evars app in *)
-	let morph = Evarutil.e_new_evar evars env app in
-(* 	let evm = Evd.evars_of !evars in *)
-(* 	let sigargs = List.map  *)
-(* 	  (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y)  *)
-(* 	  sigargs  *)
-(* 	in *)
-(* 	let appm = Reductionops.nf_evar evm appm in *)
-(* 	let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in *)
-	let proj = 
-	  mkApp (mkConst morphism_proj, 
-		Array.append cl_args [|morph|])
-	in
-	  morph, proj, sigargs, appm, morphobjs, morphobjs'
-(*       with Reduction.NotConvertible *)
-(* 	| Stdpp.Exc_located (_, Pretype_errors.PretypeError _)  *)
-(* 	| Pretype_errors.PretypeError _ -> raise Not_found *)
+    let morphargs, morphobjs = array_chop first args in
+    let morphargs', morphobjs' = array_chop first args' in
+    let appm = mkApp(m, morphargs) in
+    let appmtype = Typing.type_of env sigma appm in
+    let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
+    let cl_args = [| appmtype ; signature ; appm |] in
+    let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
+    let morph = Evarutil.e_new_evar evars env app in
+    let proj = 
+      mkApp (mkConst morphism_proj, 
+	    Array.append cl_args [|morph|])
+    in
+      morph, proj, sigargs, appm, morphobjs, morphobjs'
   in 
   let projargs, respars, typeargs = 
     array_fold_left2 
@@ -294,7 +273,7 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
     else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
 
 let resolve_all_typeclasses env evd = 
-  Eauto.resolve_all_evars env (fun x -> Typeclasses.class_of_constr x <> None) evd
+  Eauto.resolve_all_evars false (true, 15) env (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
     
 (* let _ =  *)
 (*   Typeclasses.solve_instanciation_problem := *)
@@ -319,9 +298,7 @@ let cl_rewrite_clause c left2right occs clause gl =
   let eq, _ = build_new gl env sigma occs origt newt hypt hypinfo concl (Some cstr) evars in
     match eq with  
 	Some (p, (_, _, oldt, newt)) -> 
-(* 	  evars := Typeclasses.resolve_typeclasses ~check:false env (Evd.evars_of !evars) !evars; *)
-	  evars := Classes.resolve_all_typeclasses env !evars;
-(* 	  evars := resolve_all_typeclasses env !evars; *)
+	  evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) !evars;
 	  evars := Evarutil.nf_evar_defs !evars;
 	  let p = Evarutil.nf_isevar !evars p in
 	  let newt = Evarutil.nf_isevar !evars newt in
@@ -335,11 +312,11 @@ let cl_rewrite_clause c left2right occs clause gl =
 		  refine term) gl
       | None -> tclIDTAC gl
 	  
+open Genarg
 open Extraargs
 
-
-
 TACTIC EXTEND class_rewrite
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ]
 | [ "clrewrite" orient(o) constr(c) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ None ]
@@ -358,16 +335,68 @@ TACTIC EXTEND map_tac
 | [ "clsubstitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
 END
 
+let pr_debug _prc _prlc _prt b =
+  if b then Pp.str "debug" else Pp.mt()
 
-(* 
-	  let proj = 
-	    if left2right then 
-	      let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in
-		applistc (Lazy.force proj)
-		  [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
-	    else 
-	      let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in
-		applistc (Lazy.force proj)
-		  [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
-	  in
-*)
+ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
+| [ "debug" ] -> [ true ]
+| [ ] -> [ false ]
+END
+
+let pr_mode _prc _prlc _prt m =
+  match m with
+      Some b ->
+	if b then Pp.str "depth-first" else Pp.str "breadth-fist" 
+    | None -> Pp.mt()
+	
+ARGUMENT EXTEND search_mode TYPED AS bool option PRINTED BY pr_mode
+| [ "dfs" ] -> [ Some true ]
+| [ "bfs" ] -> [ Some false ]
+| [] -> [ None ]
+END
+
+let pr_depth _prc _prlc _prt = function
+    Some i -> Util.pr_int i
+  | None -> Pp.mt()
+	
+ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
+| [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
+END
+
+let resolve_argument_typeclasses d p env evd onlyargs all =
+  let pred = 
+    if onlyargs then 
+      (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
+	class_of_constr evi.Evd.evar_concl <> None)
+    else
+      (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
+  in
+    try 
+      Eauto.resolve_all_evars d p env pred evd
+    with e -> 
+      if all then raise e else evd
+	
+VERNAC COMMAND EXTEND Typeclasses_Settings
+| [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ 
+    let mode = match s with Some t -> t | None -> true in
+    let depth = match depth with Some i -> i | None -> 15 in
+      Typeclasses.solve_instanciations_problem :=
+	resolve_argument_typeclasses d (mode, depth) ]
+END
+
+let _ = 
+  Typeclasses.solve_instanciations_problem :=
+    resolve_argument_typeclasses false (true, 15)
+      
+TACTIC EXTEND typeclasses_eauto
+| [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl ->
+    let env = pf_env gl in
+    let sigma = project gl in
+      if Evd.dom sigma = [] then Refiner.tclIDTAC gl
+      else
+	let evd = Evd.create_evar_defs sigma in
+	let mode = match s with Some t -> t | None -> true in
+	let depth = match depth with Some i -> i | None -> 15 in
+	let evd' = resolve_argument_typeclasses d (mode, depth) env evd false false in
+	  Refiner.tclEVARS (Evd.evars_of evd') gl ]
+END
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c550dbb283..70ec9d046e 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -214,8 +214,9 @@ and e_trivial_resolve db_list local_db 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 
-		      (List.hd (head_constr_bound gl [])) gl)
+  try List.map snd 
+    (e_my_find_search db_list local_db 
+	(List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
 let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
@@ -226,15 +227,18 @@ let find_first_goal gls =
 (*s The following module [SearchProblem] is used to instantiate the generic
     exploration functor [Explore.Make]. *)
       
+
+type search_state = { 
+  depth : int; (*r depth of search before failing *)
+  tacres : goal list sigma * validation;
+  last_tactic : std_ppcmds;
+  dblist : Auto.Hint_db.t list;
+  localdb :  Auto.Hint_db.t list }
+    
 module SearchProblem = struct
+    
+  type state = search_state
 
-  type state = { 
-    depth : int; (*r depth of search before failing *)
-    tacres : goal list sigma * validation;
-    last_tactic : std_ppcmds;
-    dblist : Auto.Hint_db.t list;
-    localdb :  Auto.Hint_db.t list }
-		 
   let success s = (sig_it (fst s.tacres)) = []
 
   let rec filter_tactics (glls,v) = function
@@ -316,18 +320,18 @@ end
 module Search = Explore.Make(SearchProblem)
 
 let make_initial_state n gl dblist localdb =
-  { SearchProblem.depth = n;
-    SearchProblem.tacres = tclIDTAC gl;
-    SearchProblem.last_tactic = (mt ());
-    SearchProblem.dblist = dblist;
-    SearchProblem.localdb = [localdb] }
-
-let make_initial_state_gls n gls dblist localdb =
-  { SearchProblem.depth = n;
-    SearchProblem.tacres = gls;
-    SearchProblem.last_tactic = (mt ());
-    SearchProblem.dblist = dblist;
-    SearchProblem.localdb = [localdb] }
+  { depth = n;
+    tacres = tclIDTAC gl;
+    last_tactic = (mt ());
+    dblist = dblist;
+    localdb = [localdb] }
+
+let make_initial_state_gls n gls dblist localdbs =
+  { depth = n;
+    tacres = gls;
+    last_tactic = (mt ());
+    dblist = dblist;
+    localdb = localdbs }
 
 let debug_depth_first = Search.debug_depth_first
 
@@ -335,14 +339,14 @@ let e_depth_search debug p db_list local_db gl =
   try
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
     let s = tac (make_initial_state p gl db_list local_db) in
-    s.SearchProblem.tacres
+    s.tacres
   with Not_found -> error "EAuto: depth first search failed"
 
-let e_depth_search_gls debug p db_list local_db gls =
+let e_depth_search_gls debug p db_list local_dbs gls =
   try
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
-    let s = tac (make_initial_state_gls p gls db_list local_db) in
-    s.SearchProblem.tacres
+    let s = tac (make_initial_state_gls p gls db_list local_dbs) in
+    s.tacres
   with Not_found -> error "EAuto: depth first search failed"
 
 let e_breadth_search debug n db_list local_db gl =
@@ -351,16 +355,16 @@ let e_breadth_search debug n db_list local_db gl =
       if debug then Search.debug_breadth_first else Search.breadth_first 
     in
     let s = tac (make_initial_state n gl db_list local_db) in
-    s.SearchProblem.tacres
+    s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_breadth_search_gls debug n db_list local_db gls =
+let e_breadth_search_gls debug n db_list local_dbs gls =
   try
     let tac = 
       if debug then Search.debug_breadth_first else Search.breadth_first 
     in
-    let s = tac (make_initial_state_gls n gls db_list local_db) in
-    s.SearchProblem.tacres
+    let s = tac (make_initial_state_gls n gls db_list local_dbs) in
+    s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto debug (in_depth,p) lems db_list gl = 
@@ -374,11 +378,11 @@ open Evd
 
 let e_search_auto_gls debug (in_depth,p) lems db_list gls = 
   let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
-  let local_db = make_local_hint_db lems ({it = List.hd gls'; sigma = sigma}) in
+  let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in
   if in_depth then 
-    e_depth_search_gls debug p db_list local_db gls
+    e_depth_search_gls debug p db_list local_dbs gls
   else
-    e_breadth_search_gls debug p db_list local_db gls
+    e_breadth_search_gls debug p db_list local_dbs gls
 
 let eauto debug np lems dbnames =
   let db_list =
@@ -470,33 +474,42 @@ open Evd
 
 exception Found of evar_defs
 
-let resolve_all_evars env p evd =
-  let evm = Evd.evars_of evd in
-  let goals, sigma = 
+let valid evm p res_sigma l = 
+  let evd' =
     Evd.fold
       (fun ev evi (gls, sigma) ->
-	if p evi.evar_concl then
-	  (evi :: gls, sigma)
-	else (gls, Evd.add sigma ev evi))
-      evm ([], Evd.empty)
-  in
-  let gls = { it = List.rev goals; sigma = sigma } in
-  let res_sigma = ref sigma in
-  let valid l = 
-    let evd' =
-      Evd.fold
-	(fun ev evi (gls, sigma) ->
-	  if p evi.evar_concl then
-	    match gls with
-		hd :: tl -> 
+	if not (Evd.is_evar evm ev) then
+	  match gls with
+	      hd :: tl -> 
+		if evi.evar_body = Evar_empty then
 		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
-		  (tl, Evd.evar_define ev cstr sigma)
-	      | [] -> assert(false)
-	  else (gls, sigma))
-	evm (l, evd)
-    in raise (Found (snd evd'))
-  in
-  let gls', valid' = full_eauto_gls true (false, 10) [] (gls, valid) in
-    res_sigma := sig_sig gls';
-    try ignore(valid' []); assert(false) with Found evd' -> evd'
+		    (tl, Evd.evar_define ev cstr sigma)
+		else (tl, sigma)
+	    | [] -> ([], sigma)
+	else if not (Evd.is_defined evm ev) && p ev evi then
+	  match gls with
+	      hd :: tl -> 
+		if evi.evar_body = Evar_empty then
+		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
+		    (tl, Evd.evar_define ev cstr sigma)
+		else (tl, sigma)
+	    | [] -> assert(false)
+	else (gls, sigma))
+      !res_sigma (l, Evd.create_evar_defs !res_sigma)
+  in raise (Found (snd evd'))
     
+let resolve_all_evars debug (mode, depth) env p evd =
+  let evm = Evd.evars_of evd in
+  let goals = 
+    Evd.fold
+      (fun ev evi gls ->
+	if evi.evar_body = Evar_empty && p ev evi then
+	  (evi :: gls)
+	else gls)
+      evm []
+  in
+  let gls = { it = List.rev goals; sigma = evm } in
+  let res_sigma = ref evm in
+  let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in
+    res_sigma := Evarutil.nf_evars (sig_sig gls');
+    try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 34c4cab78b..940648c2eb 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -14,6 +14,7 @@ open Auto
 open Topconstr
 open Evd
 open Environ
+open Explore
 (*i*)
 
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
@@ -26,10 +27,47 @@ val registered_e_assumption : tactic
 
 val e_give_exact_constr : constr -> tactic
 
+type search_state = { 
+  depth : int; (*r depth of search before failing *)
+  tacres : goal list sigma * validation;
+  last_tactic : Pp.std_ppcmds;
+  dblist : Auto.Hint_db.t list;
+  localdb :  Auto.Hint_db.t list }
+
+module SearchProblem : sig
+  type state = search_state
+      
+  val filter_tactics :     Proof_type.goal list Tacmach.sigma * (Proof_type.proof_tree list -> 'a) ->
+    (Tacmach.tactic * Pp.std_ppcmds) list ->
+    ((Proof_type.goal list Tacmach.sigma * (Proof_type.proof_tree list -> 'a)) *
+     Pp.std_ppcmds)
+    list
+
+  val compare :  search_state -> search_state -> int
+
+  val branching : state -> state list
+  val success : state -> bool
+  val pp : state -> unit
+end
+
+module Search : sig
+  val depth_first : search_state -> search_state
+  val debug_depth_first : search_state -> search_state
+
+  val breadth_first : search_state -> search_state
+  val debug_breadth_first : search_state -> search_state
+end
+
 val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation -> 
   goal list sigma * validation
 
-val resolve_all_evars : env -> (constr -> bool) -> evar_defs -> evar_defs
+val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
+  evar_defs
+
+val valid :     Evd.evar_map ->
+    (Evd.evar -> Evd.evar_info -> bool) ->
+    Evd.evar_map ref -> Proof_type.proof_tree list -> 'a
+
 
 val gen_eauto : bool -> bool * int -> constr list -> 
   hint_db_name list option -> tactic
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index aec2608735..beeb745899 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -1 +1,18 @@
-Ltac typeclass_instantiation := eauto with typeclass_instances || eauto.
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Initialization code for typeclasses, setting up the default tactic 
+   for instance search.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: Init.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index 694cab59bc..aaeb186545 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -77,7 +77,7 @@ Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R
 
 Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; eapply symmetric ; eauto.
+  Solve Obligations using unfold flip ; program_simpl ; apply symmetric ; eauto.
 
 Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R).
   
@@ -320,12 +320,12 @@ Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) :=
 Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => 
   flip_antisymmetric : ? Antisymmetric eq (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
 
 Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => 
   inverse_antisymmetric : ? Antisymmetric eq (inverse R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply antisymmetric ; eauto.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 92a5dfc8b7..959dc10404 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -256,8 +256,8 @@ let new_class id par ar sup props =
   (* Instantiate evars and check all are resolved *)
   let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in
   let sigma = Evd.evars_of isevars in
-  let ctx_params = Implicit_quantifiers.nf_named_context sigma ctx_params in
-  let ctx_props = Implicit_quantifiers.nf_named_context sigma ctx_props in
+  let ctx_params = Evarutil.nf_named_context_evar sigma ctx_params in
+  let ctx_props = Evarutil.nf_named_context_evar sigma ctx_props in
   let arity = Reductionops.nf_evar sigma arity in
   let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
   let kn = 
@@ -404,7 +404,7 @@ let new_instance ctx (instid, bk, cl) props =
   let sigma = Evd.evars_of !isevars in
   isevars := resolve_typeclasses env sigma !isevars;
   let sigma = Evd.evars_of !isevars in
-  let env' = Implicit_quantifiers.nf_env sigma env' in
+  let env' = Evarutil.nf_env_evar sigma env' in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, propsctx = 
     let props = 
@@ -474,7 +474,7 @@ let context l =
   let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  let fullctx = Implicit_quantifiers.nf_named_context sigma (l @ ctx) in
+  let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
     List.iter (function (id,_,t) -> 
       Command.declare_one_assumption false (Local (* global *), Definitional) t false (* inline *) (dummy_loc, id))
       (List.rev fullctx)
@@ -493,34 +493,34 @@ let _ =
       Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
       solve_by_tac env evd ev evi (Lazy.force tactic))
 
-let prod = lazy (Coqlib.build_prod ())
-
-let build_conjunction evm =
-  List.fold_left
-    (fun (acc, evs) (ev, evi)  ->
-      if class_of_constr evi.evar_concl <> None then
-	mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs
-      else acc, Evd.add evs ev evi)
-    (Coqlib.build_coq_True (), Evd.empty) evm
-
-let destruct_conjunction evm_list evm evm' term =
-  let _, evm =
-    List.fold_right
-      (fun (ev, evi) (term, evs) ->
-	if class_of_constr evi.evar_concl <> None then
-	  match kind_of_term term with
-	    | App (x, [| _ ; _ ; proof ; term |]) ->
-		let evs' = Evd.define evs ev proof in
-		  (term, evs')
-	    | _ -> assert(false)
-	else
-	  match (Evd.find evm' ev).evar_body with
-	      Evar_empty -> raise Not_found
-	    | Evar_defined c ->
-		let evs' = Evd.define evs ev c in
-		  (term, evs'))
-      evm_list (term, evm)
-  in evm
+(* let prod = lazy_fun Coqlib.build_prod *)
+
+(* let build_conjunction evm = *)
+(*   List.fold_left *)
+(*     (fun (acc, evs) (ev, evi)  -> *)
+(*       if class_of_constr evi.evar_concl <> None then *)
+(* 	mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs *)
+(*       else acc, Evd.add evs ev evi) *)
+(*     (Coqlib.build_coq_True (), Evd.empty) evm *)
+
+(* let destruct_conjunction evm_list evm evm' term = *)
+(*   let _, evm = *)
+(*     List.fold_right *)
+(*       (fun (ev, evi) (term, evs) -> *)
+(* 	if class_of_constr evi.evar_concl <> None then *)
+(* 	  match kind_of_term term with *)
+(* 	    | App (x, [| _ ; _ ; proof ; term |]) -> *)
+(* 		let evs' = Evd.define evs ev proof in *)
+(* 		  (term, evs') *)
+(* 	    | _ -> assert(false) *)
+(* 	else *)
+(* 	  match (Evd.find evm' ev).evar_body with *)
+(* 	      Evar_empty -> raise Not_found *)
+(* 	    | Evar_defined c -> *)
+(* 		let evs' = Evd.define evs ev c in *)
+(* 		  (term, evs')) *)
+(*       evm_list (term, evm) *)
+(*   in evm *)
  
 (* let solve_by_tac env evd evar evi t = *)
 (*   let goal = {it = evi; sigma = (Evd.evars_of evd) } in *)
@@ -535,17 +535,32 @@ let destruct_conjunction evm_list evm evm' term =
 (* 	else evd, false *)
 (*     else evd, false *)
 
-let resolve_all_typeclasses env evd =
-  let evm = Evd.evars_of evd in
-  let evm_list = Evd.to_list evm in
-  let goal, typesevm = build_conjunction evm_list in
-  let evars = ref (Evd.create_evar_defs typesevm) in
-  let term = resolve_one_typeclass_evd env evars goal in
-  let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in
-    Evd.create_evar_defs evm'
-
-let _ =
-  Typeclasses.solve_instanciations_problem :=
-    (fun env evd -> 
-      Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
-      resolve_all_typeclasses env evd)
+(* let resolve_all_typeclasses env evd = *)
+(*   let evm = Evd.evars_of evd in *)
+(*   let evm_list = Evd.to_list evm in *)
+(*   let goal, typesevm = build_conjunction evm_list in *)
+(*   let evars = ref (Evd.create_evar_defs typesevm) in *)
+(*   let term = resolve_one_typeclass_evd env evars goal in *)
+(*   let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in *)
+(*     Evd.create_evar_defs evm' *)
+
+(* let _ = *)
+(*   Typeclasses.solve_instanciations_problem := *)
+(*     (fun env evd ->  *)
+(*       Library.require_library [(dummy_loc, module_qualid)] None; (\* may be inefficient *\) *)
+(*       resolve_all_typeclasses env evd) *)
+
+let solve_evars_by_tac env evd t =
+  let ev = make_evar empty_named_context_val mkProp in
+  let goal = {it = ev; sigma = (Evd.evars_of evd) } in
+  let (res, valid) = t goal in 
+  let evd' = evars_reset_evd res.sigma evd in
+    evd'
+(*       Library.require_library [(dummy_loc, module_qualid)] None (a\* may be inefficient *\); *)
+
+(* let _ = *)
+(*   Typeclasses.solve_instanciations_problem := *)
+(*     (fun env evd ->  *)
+(*       Eauto.resolve_all_evars false (true, 15) env  *)
+(* 	(fun ev evi -> is_implicit_arg (snd (evar_source ev evd)) *)
+(* 	  && class_of_constr evi.evar_concl <> None) evd) *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index cfe881cb31..015bdce5c3 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -62,6 +62,11 @@ val solve_by_tac :     env ->
   Proof_type.tactic ->
     Evd.evar_defs * bool
 
+val solve_evars_by_tac :     env ->
+    Evd.evar_defs ->
+  Proof_type.tactic ->
+  Evd.evar_defs
+
 val decompose_named_assum : types -> named_context * types
 
 val push_named_context : named_context -> env -> env
@@ -69,5 +74,3 @@ val push_named_context : named_context -> env -> env
 val name_typeclass_binders : Idset.t ->
     Topconstr.local_binder list ->
     Topconstr.local_binder list * Idset.t
-
-val resolve_all_typeclasses : env -> evar_defs -> evar_defs