Fix interface of resolve_typeclasses: onlyargs -> with_goals:

by default typeclass resolution is not launched on goal evars.

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

5 files changed, 13 insertions, 15 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3277456163..560b615467 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -323,7 +323,7 @@ let coerce_itf loc env isevars v t c1 =
 
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
-    ~onlyargs:true ~split:true ~fail:false env evd
+    ~with_goals:false ~split:true ~fail:false env evd
 
 (* appliquer le chemin de coercions p à hj *)
 let apply_coercion env sigma p hj typ_cl =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d96f47e3f2..0205a52d5d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -105,10 +105,8 @@ let interp_elimination_sort = function
 
 let resolve_evars env evdref fail_evar resolve_classes =
   if resolve_classes then
-    (evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
-       ~split:true ~fail:true env !evdref;
-     evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
-       ~split:true ~fail:fail_evar env !evdref);
+    (evdref := Typeclasses.resolve_typeclasses ~with_goals:false
+     ~split:true ~fail:fail_evar env !evdref);
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
 	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index be335ac913..e6005391da 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -451,11 +451,11 @@ let is_instance = function
       is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg k =
-  match k with
-      ImplicitArg (ref, (n, id), b) -> true
-    | InternalHole -> true
-    | _ -> false
+let is_implicit_arg k = k <> GoalEvar
+  (* match k with *)
+  (*     ImplicitArg (ref, (n, id), b) -> true *)
+  (*   | InternalHole -> true *)
+  (*   | _ -> false *)
 
 
 (* To embed a boolean for resolvability status.
@@ -500,6 +500,6 @@ let has_typeclasses evd =
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 
-let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
+let resolve_typeclasses ?(with_goals=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses evd) then evd
-  else !solve_instanciations_problem env evd onlyargs split fail
+  else !solve_instanciations_problem env evd with_goals split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 67336b3407..b1db243d67 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -80,7 +80,7 @@ val is_implicit_arg : hole_kind -> bool
 val instance_constructor : typeclass -> constr list -> constr option * types
 
 (** Resolvability.
-    Only undefined evars could be marked or checked for resolvability. *)
+    Only undefined evars can be marked or checked for resolvability. *)
 
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
@@ -89,7 +89,7 @@ val mark_resolvable : evar_info -> evar_info
 val mark_resolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
-val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
+val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 983b9fd618..ce0af6853a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -966,7 +966,7 @@ let check_types env flags (sigma,_,_ as subst) m n =
 
 let try_resolve_typeclasses env evd flags m n =
   if flags.resolve_evars then
-    try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
+    try Typeclasses.resolve_typeclasses ~with_goals:false ~split:false
 	  ~fail:true env evd
     with e when Typeclasses_errors.unsatisfiable_exception e ->
       error_cannot_unify env evd (m, n)