diff options
| author |  Robbert Krebbers <mail@robbertkrebbers.nl> | 2017-11-14 22:48:54 +0100 |
|---|---|---|
| committer | Robbert Krebbers <mail@robbertkrebbers.nl> | 2017-11-14 22:50:08 +0100 |
| commit | edc5d8f0c6128949521fa331e55cc67084951bfb (patch) | |
| tree | 41634b99869dc7f68137755223e462beff4824bb /theories/QArith/Qreals.v | |
| parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) | |
Get rid of ' notation for Zpos in QArith.
Diffstat (limited to 'theories/QArith/Qreals.v')
| -rw-r--r-- | theories/QArith/Qreals.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index e6f7e7ac9..c5059489e 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -165,8 +165,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. intros; field; auto. intros; - change (IZR (Zneg x2)) with (- IZR (' x2))%R; - change (IZR (Zneg p)) with (- IZR (' p))%R; + change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R; + change (IZR (Zneg p)) with (- IZR (Zpos p))%R; simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. |