diff options
| author | Hugo Herbelin | 2019-11-14 12:14:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:41 +0100 |
| commit | 3eea1e383e23ea76fcd49a7b302f31b2e3f6ef2a (patch) | |
| tree | 3dd02ed247398092b461bac6612ff4a07e45c6bc /interp/notation_ops.ml | |
| parent | ba52fd0dff4dcf06621fb91ff4902a060a0b222d (diff) | |
Fix inheritance of argument scopes when printing notations in patterns.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions