From e1ef9491edaf8f7e6f553c49b24163b7e2a53825 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 5 Mar 2017 21:03:51 +0100
Subject: Change the parser and printer so that they use IZR for real
 constants.

There are two main issues. First, (-cst)%R is no longer syntactically
equal to (-(cst))%R (though they are still convertible). This breaks some
rewriting rules.

Second, the ring/field_simplify tactics did not know how to refold
real constants. This defect is no longer hidden by the pretty-printer,
which makes these tactics almost unusable on goals containing large
constants.

This commit also modifies the ring/field tactics so that real constant
reification is now constant time rather than linear.

Note that there is now a bit of code duplication between z_syntax and
r_syntax. This should be fixed once plugin interdependencies are supported.

Ideally the r_syntax plugin should just disappear by declaring IZR as a
coercion. Unfortunately the coercion mechanism is not powerful enough yet,
be it for parsing (need the ability for a scope to delegate constant
parsing to another scope) or printing (too many visible coercions left).
---
 plugins/fourier/Fourier.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 1d7ee93ea3..a962547131 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -13,6 +13,6 @@ Require Export DiscrR.
 Require Export Fourier_util.
 Declare ML Module "fourier_plugin".
 
-Ltac fourier := abstract (fourierz; field; discrR).
+Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).
 
 Ltac fourier_eq := apply Rge_antisym; fourier.
-- 
cgit v1.2.3