From 8e65ca556c907185a6e6da4aaf23babb198aad1c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Oct 2014 17:02:18 +0200
Subject: Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars
 by names): VarInstance behaves like GoalEvar for type class resolution.

---
 pretyping/typeclasses.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8b6fe90c0a..8217a65a24 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -527,7 +527,7 @@ open Evar_kinds
 type evar_filter = existential_key -> Evar_kinds.t -> bool
 
 let all_evars _ _ = true
-let all_goals _ = function GoalEvar -> true | _ -> false
+let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false
 let no_goals ev evi = not (all_goals ev evi)
 let no_goals_or_obligations _ = function
   | VarInstance _ | GoalEvar | QuestionMark _ -> false
-- 
cgit v1.2.3