diff options
| author | Arnaud Spiwack | 2015-10-30 10:06:24 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-10-30 10:06:24 +0100 |
| commit | 441ea07e3c8ba56b9e7d44e7802246dc06814415 (patch) | |
| tree | 6f5b75969e49ab97e4ed1e03f8d09bed68306be5 /interp/notation.ml | |
| parent | 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 (diff) | |
More uniformity in the style of comparison functions.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions