From a4a76c253474ac4ce523b70d0150ea5dcf546385 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 5 Mar 2017 20:48:52 +0100
Subject: Make IZR use a compact representation of integers.

That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not
convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means
that, after reduction, real constants no longer exponentially blow up.

Note that I was not able to fix the test-suite for the declarative mode,
so the missing proof terms have been admitted.
---
 test-suite/success/decl_mode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
index 58f79d45ec..e569bcb49f 100644
--- a/test-suite/success/decl_mode.v
+++ b/test-suite/success/decl_mode.v
@@ -153,7 +153,7 @@ proof.
       thus ~= (IZR (Zneg z) * IZR (Zneg z)).
   end cases.
 end proof.
-Qed.
+Admitted.
 
 Definition irrational (x:R):Prop :=
   forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q).
-- 
cgit v1.2.3