aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-09-17 11:42:05 +0200
committerMatthieu Sozeau2014-09-17 12:37:02 +0200
commit9de1edd730eeb3cada742a27a36bc70178eda6d8 (patch)
tree341d93576b40d8fc4bb2e6abd6096a69df6b09a6 /dev
parentd34e1eed232c84590ddb80d70db9f7f7cf13584a (diff)
While resolving typeclass evars in clenv, touch only the ones that appear in the
clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions