From bedbdbc3daf27f80252ac2c7a968b1cc2730ad83 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Mar 2017 14:53:54 +0200 Subject: Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. --- theories/Reals/RIneq.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Reals') diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index dd2108159..8bebb5237 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -2017,7 +2017,7 @@ Proof. Qed. Lemma R_rm : ring_morph - R0 R1 Rplus Rmult Rminus Ropp eq + 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR. Proof. constructor ; try easy. -- cgit v1.2.3