From 7e1243a174e28535d9b35b558ed94f1548acd78c Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 13 Oct 2018 22:17:27 +0200
Subject: 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.
---
 plugins/setoid_ring/RealField.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins/setoid_ring')

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
-- 
cgit v1.2.3