aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2016-07-18 15:09:08 +0200
committerHugo Herbelin2016-07-18 15:51:02 +0200
commitfd0cd480a720cbba15de86bbc9cad74ba6d89675 (patch)
tree157da3e6f8a88f752fe516e34d70d58a7864021c /dev
parent2042daa9a6e13cbb9636a62812015749d95c2283 (diff)
A new step on using alpha-conversion in printing notations.
A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions