diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-08 12:22:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-08 12:26:33 +0200 |
| commit | 822ca6f64bd30a1ee3a2417af3c66711326b7d38 (patch) | |
| tree | fd23e7c1f20f60812493824f34912ac42a470686 /theories/QArith | |
| parent | eb7753109a849aaa7fe5c341f02e408c5fc49f85 (diff) | |
Fixing bug #3270. Patch by Robbert Krebbers.
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/Qcanon.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index f0edc9f13..2ed7a29ea 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -70,7 +70,6 @@ Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). Arguments Q2Qc q%Q. -Notation " !! " := Q2Qc : Qc_scope. Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. Proof. @@ -87,8 +86,8 @@ Proof. Qed. Hint Resolve Qc_is_canon. -Notation " 0 " := (!!0) : Qc_scope. -Notation " 1 " := (!!1) : Qc_scope. +Notation " 0 " := (Q2Qc 0) : Qc_scope. +Notation " 1 " := (Q2Qc 1) : Qc_scope. Definition Qcle (x y : Qc) := (x <= y)%Q. Definition Qclt (x y : Qc) := (x < y)%Q. @@ -144,15 +143,15 @@ Defined. (** The addition, multiplication and opposite are defined in the straightforward way: *) -Definition Qcplus (x y : Qc) := !!(x+y). +Definition Qcplus (x y : Qc) := Q2Qc (x+y). Infix "+" := Qcplus : Qc_scope. -Definition Qcmult (x y : Qc) := !!(x*y). +Definition Qcmult (x y : Qc) := Q2Qc (x*y). Infix "*" := Qcmult : Qc_scope. -Definition Qcopp (x : Qc) := !!(-x). +Definition Qcopp (x : Qc) := Q2Qc (-x). Notation "- x" := (Qcopp x) : Qc_scope. Definition Qcminus (x y : Qc) := x+-y. Infix "-" := Qcminus : Qc_scope. -Definition Qcinv (x : Qc) := !!(/x). +Definition Qcinv (x : Qc) := Q2Qc (/x). Notation "/ x" := (Qcinv x) : Qc_scope. Definition Qcdiv (x y : Qc) := x*/y. Infix "/" := Qcdiv : Qc_scope. |