diff options
| author | Hugo Herbelin | 2017-08-15 18:19:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:05 +0100 |
| commit | ecc5658d7efd3a79a6309be6440d1005d30e6285 (patch) | |
| tree | d8aa172cb495509266758b55150c08c2134b425c /interp/notation_ops.mli | |
| parent | bfed8dcbe7f91ec65ae5e6d1c0a2f06ca7fa01f6 (diff) | |
Preliminary work before adding general support for patterns in notations I.
Factorizing the place where the different form of extended binders
(i.e. possibly including the 'pat form) are matched.
Diffstat (limited to 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions