diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-18 16:15:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-18 16:40:24 +0200 |
| commit | 6d549d3a2b0ab89c77e34646e866584522bd3591 (patch) | |
| tree | 003b5f74bb978949c2a048ad6dfb8015a4c7dcc3 /pretyping/typeclasses.ml | |
| parent | 870d81c699b5d15420a03f2006a7938a158c09a8 (diff) | |
For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop in Class_tactics).
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a391a785c..8b6fe90c0 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 = |