aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2017-05-30 12:10:35 +0200
committerThéo Zimmermann2017-05-30 12:11:04 +0200
commite6c41b96a5ea9f8559acf176cdf997b05ccfb317 (patch)
treed0b596966abb0d69a37448c481d68140edc63bd7 /API/API.mli
parenteefda76f6f42674fb342e1aa5f1dcf29569a4806 (diff)
Fix bug 5550: "typeclasses eauto with" does not work with section variables.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions