diff options
| author | Pierre Letouzey | 2017-03-07 12:31:29 +0100 |
|---|---|---|
| committer | Jason Gross | 2018-02-20 19:12:35 -0500 |
| commit | 0f2b6099073ef9494f09cfd68edfd64508561b62 (patch) | |
| tree | 313cfe0aa47b149051a5585590b24cf0ca04f543 /doc | |
| parent | c1d4048a12441df2977965b186bae9dcd32d4129 (diff) | |
Decimal goodies : conversion to/from Coq strings
Just because it's fun and easy. Not used by the Numeral Notation command.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions