From debb1dba19c079afd7657e8518034209f08bb2b1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 20 Mar 2012 18:46:08 +0000
Subject: 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
---
 pretyping/typeclasses.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'pretyping/typeclasses.ml')

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
-- 
cgit v1.2.3