diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 15:23:47 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-15 15:47:39 +0200 |
| commit | d03f927e1f2d066b8fdd1e156cb98a40f8dab89d (patch) | |
| tree | 350334d43cad7bb1613f9666a715f2fe836a34d1 /tactics/class_tactics.ml | |
| parent | 9097aed0e4a6af73646376ee6a24f96944a1a78e (diff) | |
Fix for bug #3618.
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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' |