From d03f927e1f2d066b8fdd1e156cb98a40f8dab89d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Oct 2014 15:23:47 +0200 Subject: Fix for bug #3618. Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars. --- tactics/class_tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/class_tactics.ml') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 38f1114b5..344597fcd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -382,7 +382,7 @@ let hints_tac hints = let sgls = evars_to_goals (fun evm ev evi -> - if Typeclasses.is_resolvable evi && + if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && (not info.only_classes || Typeclasses.is_class_evar evm evi) then Typeclasses.mark_unresolvable evi, true else evi, false) s' -- cgit v1.2.3