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/Qcanon.v | |
| parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) | |
Get rid of ' notation for Zpos in QArith.
Diffstat (limited to 'theories/QArith/Qcanon.v')
| -rw-r--r-- | theories/QArith/Qcanon.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 0b399febe..527c3f344 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -28,7 +28,7 @@ Lemma Qred_identity : Proof. intros (a,b) H; simpl in *. rewrite <- Z.ggcd_gcd in H. - generalize (Z.ggcd_correct_divisors a ('b)). + generalize (Z.ggcd_correct_divisors a (Zpos b)). destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst. rewrite !Z.mul_1_l. now intros (<-,<-). Qed. @@ -37,7 +37,7 @@ Lemma Qred_identity2 : forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. intros (a,b) H; simpl in *. - generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. injection H as <- <-. intros H (_,H'). |