diff options
| author | Emilio Jesus Gallego Arias | 2020-06-19 20:34:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-27 19:03:33 +0200 |
| commit | 694afd3fe8b03ebf73c06c62ac97c9737f60d551 (patch) | |
| tree | 6dbf00dc3a43576f686ba60edee3ce0c4a079d1e /plugins/syntax/float_syntax.ml | |
| parent | 3fcd90f590bf0b40e24e20d18f96776232cb014e (diff) | |
[numtok] [zarith] Simplifications
Suggested by Pierre Roux
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions