diff options
| author | Pierre Roux | 2018-10-13 22:17:27 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:25 +0200 |
| commit | 7e1243a174e28535d9b35b558ed94f1548acd78c (patch) | |
| tree | 3f4176549aa679f99e7d9dd71397b1cf0daa2279 /kernel/type_errors.mli | |
| parent | 552bb5aba750785d8f19aa7b333baa59e9199369 (diff) | |
Make R parser parse decimals (e.g., 1.02e+01)
RealField.v is slightly modified so that the ring/field tactics
consider the term (IZR (Z.pow_pos 10 _)) produced when parsing
exponents as constants.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions