diff options
| author | Emilio Jesus Gallego Arias | 2019-04-05 01:28:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-05 01:28:47 +0200 |
| commit | be6f3a6234ee809dd3c290621d80c3280a41355e (patch) | |
| tree | 8fed697f726193b765c8a2faeedd34ad60b541cb /plugins/setoid_ring | |
| parent | 2e1aa5c15ad524cffd03c7979992af44ab2bb715 (diff) | |
| parent | 6af420bb384af0acf94028fc44ef44fd5a6fd841 (diff) | |
Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
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 |