diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 11:00:20 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 11:00:20 +0100 |
| commit | 16f93d201cf7e379d5acf533be20fed30bbc212c (patch) | |
| tree | a4d1e8ee095c3892f98e80860010f118ab9e8558 /theories/QArith/Qreals.v | |
| parent | a4f37da927bc267de505da12f5e5d626af219f90 (diff) | |
| parent | f4e46fdf6072727cbfdef42a6db77d5be05d027a (diff) | |
Merge PR #6155: 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 14ab1700e..c83296259 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -167,8 +167,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. |