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

3 files changed, 11 insertions, 11 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index cf9c90e17..f60598844 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 aba11231c..84d374028 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 a59d2483e..5bcbf4db6 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