diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-30 14:53:54 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-30 14:53:54 +0200 |
| commit | bedbdbc3daf27f80252ac2c7a968b1cc2730ad83 (patch) | |
| tree | 3475adff21863cc276eefbbb5d1568b2ea454bb6 /theories/Reals | |
| parent | ab9e14c9e61aee9812a1b30795942a0a2bea63de (diff) | |
Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/RIneq.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |