diff options
| author | Théo Zimmermann | 2019-12-22 20:52:01 +0100 |
|---|---|---|
| committer | GitHub | 2019-12-22 20:52:01 +0100 |
| commit | 273586eca1f6372d3b633b7689b9cbb33d4e79ea (patch) | |
| tree | 1fe7b221a0894d4be23ce6bc42a72c0915fb60ec /interp/notation.ml | |
| parent | 6a148b1b876906cdea6ed74dc80789f8a3ea16e6 (diff) | |
Apply suggestions from code review
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions