aboutsummaryrefslogtreecommitdiffhomepage
path: root/clib
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-15 01:04:51 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:05 +0100
commit00bfd6fa443232bc908cfa13553e2fa1cf783ffa (patch)
tree6790ecc2f7b4e6882d049d751f63fc3bc761f0ef /clib
parent6480c7e1d89558252f2e8a8f1b7d3b03f7ef6a74 (diff)
Preliminary work before extending support for binders in notations
(binders shall be substitutable by arbitrary cases patterns).
Diffstat (limited to 'clib')
0 files changed, 0 insertions, 0 deletions