aboutsummaryrefslogtreecommitdiffhomepage
path: root/README
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-15 15:23:47 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-15 15:47:39 +0200
commitd03f927e1f2d066b8fdd1e156cb98a40f8dab89d (patch)
tree350334d43cad7bb1613f9666a715f2fe836a34d1 /README
parent9097aed0e4a6af73646376ee6a24f96944a1a78e (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 'README')
0 files changed, 0 insertions, 0 deletions