diff options
| author | Hugo Herbelin | 2018-05-10 14:57:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-05-10 15:19:06 +0200 |
| commit | dfa99b152114271cf9fac4cab9d8663ac6ec078c (patch) | |
| tree | 80e8af6b339a263580cf1ad4c70c0e3269b4f89c /interp/notation.mli | |
| parent | e559f7553030dc3a86936794d0f80f39b0131960 (diff) | |
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions