aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1680.v
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-17 11:42:05 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-17 12:37:02 +0200
commit9de1edd730eeb3cada742a27a36bc70178eda6d8 (patch)
tree341d93576b40d8fc4bb2e6abd6096a69df6b09a6 /test-suite/bugs/closed/1680.v
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 'test-suite/bugs/closed/1680.v')
0 files changed, 0 insertions, 0 deletions