diff options
| author | Hugo Herbelin | 2017-08-15 01:04:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:05 +0100 |
| commit | 00bfd6fa443232bc908cfa13553e2fa1cf783ffa (patch) | |
| tree | 6790ecc2f7b4e6882d049d751f63fc3bc761f0ef /interp/notation_ops.ml | |
| parent | 6480c7e1d89558252f2e8a8f1b7d3b03f7ef6a74 (diff) | |
Preliminary work before extending support for binders in notations
(binders shall be substitutable by arbitrary cases patterns).
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions