aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorHugo Herbelin2020-10-24 14:45:25 +0200
committerHugo Herbelin2020-11-20 20:02:35 +0100
commit3e6b9a0da40b1302b08a1e34e2f879ba6fd5bb15 (patch)
tree3c09e49b3fa3b62056b7b356bdaf891c15e77cf8 /doc
parent7508be4f6d61dd2735ff0b8d406a6a66cd2faad9 (diff)
Tests for notations with general single (non-recursive) binders.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions