| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-01-28 | Fix #11467 | Pierre Roux | |
| 'e' was not displayed when printing decimal notations in R : Require Import Reals. Check (1.23e1, 32e+1, 0.1)%R. was giving < (123-1%R, 321%R, 1-1%R) instead of < (123e-1%R, 32e1%R, 1e-1%R) This was introduced in #8764 (in Coq 8.10). | |||
| 2019-04-02 | Make R parser parse decimals (e.g., 1.02e+01) | Pierre Roux | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |