aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/RealSyntax.v
AgeCommit message (Collapse)Author
2019-04-02Make 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.