diff options
| author | Arnaud Spiwack | 2014-12-12 09:28:23 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-12 19:21:56 +0100 |
| commit | a5ccde6f22deb1a1a2d59d3b532f74c217a05aee (patch) | |
| tree | 61ec37224340213b6be70024ea55b80f5d4b6d68 /plugins/syntax/string_syntax.ml | |
| parent | ed89c1ee0d24d0e4356e77561bab4822125db057 (diff) | |
Make sure the goals on the shelve are identified as goal and unresolvable for typeclasses.
This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.
Fixes #3841.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions