diff options
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 |