diff options
| author | Pierre Roux | 2021-02-09 18:23:11 +0100 |
|---|---|---|
| committer | Pierre Roux | 2021-02-27 12:07:39 +0100 |
| commit | c02bbaeb9c6c9cbc4a7f2dc47876a94fdd33aa5e (patch) | |
| tree | f2288e6e102d9711b2e327cbd2502ecd109ae15d /kernel/vmlambda.ml | |
| parent | 3915bc904fc16060c25baaf7d5626e3587ad2891 (diff) | |
Remove decimal-only number notations
This was deprecated in 8.12
Diffstat (limited to 'kernel/vmlambda.ml')
0 files changed, 0 insertions, 0 deletions