diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-03-07 12:31:29 +0100 |
|---|---|---|
| committer |  Jason Gross <jgross@mit.edu> | 2018-02-20 19:12:35 -0500 |
| commit | 0f2b6099073ef9494f09cfd68edfd64508561b62 (patch) | |
| tree | 313cfe0aa47b149051a5585590b24cf0ca04f543 /dev/Coq_Bugzilla_autolink.user.js | |
| 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 'dev/Coq_Bugzilla_autolink.user.js')
0 files changed, 0 insertions, 0 deletions