diff options
| author | Hugo Herbelin | 2017-08-18 09:50:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:05 +0100 |
| commit | e21f70cc2b284a3cf489b16e0251492fb864cf1e (patch) | |
| tree | a071e82af9ce82af1baff18ea46f06318462eb5c /interp/notation_ops.mli | |
| parent | ecc5658d7efd3a79a6309be6440d1005d30e6285 (diff) | |
Preliminary work before adding general support for patterns in notations II.
Reordering the maps for binders and terms while uninterpreting a
notation the same way it will be at the time of interpreting a
notation.
Diffstat (limited to 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions