diff options
| author | Antonio Nikishaev | 2020-05-13 15:51:32 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-05-13 15:51:32 +0400 |
| commit | 7510aa6d49cbc48962ee29949b61f1bed2b27e1a (patch) | |
| tree | 0f3ebcbaf2beb595eb59d3e1cba924eb4725f5f7 /plugins/syntax/float_syntax.ml | |
| parent | 38c522dcd78c7b62ad2017ee1eaff864e377e299 (diff) | |
do not re-export ListNotations from Program: kill overlays
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions