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 /plugins/setoid_ring | |
| 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 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/RealField.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 38bc58a659..e12bf36339 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -141,6 +141,11 @@ Ltac IZR_tac t := match t with | R0 => constr:(0%Z) | R1 => constr:(1%Z) + | IZR (Z.pow_pos 10 ?p) => + match isPcst p with + | true => constr:(Z.pow_pos 10 p) + | _ => constr:(InitialRing.NotConstant) + end | IZR ?u => match isZcst u with | true => u |