diff options
| author | Hugo Herbelin | 2020-04-15 15:47:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-05 19:09:07 +0100 |
| commit | 4b8a87bcebe23797c4a179dd6a1d55c058d2736f (patch) | |
| tree | cf7fe25ea299c7a39ff6b962dea1b2c8af2b547c /interp/notation_ops.ml | |
| parent | cb105b62f597b2a51fad743547647e4885d6365a (diff) | |
Passing full interning env to pattern interning, for better control.
This will allow for instance to check the status of a variable name
used both as a term and binder in notations.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions