From 6d549d3a2b0ab89c77e34646e866584522bd3591 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 18 Sep 2014 16:15:34 +0200
Subject: For type classes, tell that VarInstance's behave like GoalEvar (avoid
 a loop in Class_tactics).

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

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index a391a785cc..8b6fe90c0a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -530,7 +530,7 @@ let all_evars _ _ = true
 let all_goals _ = function GoalEvar -> true | _ -> false
 let no_goals ev evi = not (all_goals ev evi)
 let no_goals_or_obligations _ = function
-  | GoalEvar | QuestionMark _ -> false
+  | VarInstance _ | GoalEvar | QuestionMark _ -> false
   | _ -> true
 
 let mark_resolvability filter b sigma =
-- 
cgit v1.2.3