diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/algebra/rat.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/algebra/rat.v')
| -rw-r--r-- | mathcomp/algebra/rat.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 7945265..3db328d 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -294,7 +294,7 @@ Proof. by move=> x y /=; rewrite !ratz_frac mulq_frac // /= !mulr1. Qed. Fact invq_frac x : x.1 != 0 -> x.2 != 0 -> invq (fracq x) = fracq (invq_subdef x). Proof. -by rewrite /invq_subdef; case: fracqP => // k {x} x k0; rewrite fracqMM. +by rewrite /invq_subdef; case: fracqP => // k {}x k0; rewrite fracqMM. Qed. Fact mulqC : commutative mulq. @@ -357,7 +357,7 @@ Canonical rat_countFieldType := [countFieldType of rat]. Lemma numq_eq0 x : (numq x == 0) = (x == 0). Proof. -rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {x} x k0]. +rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {}x k0]. by rewrite eqxx orbT. by rewrite !mulf_eq0 (negPf k0) /= denq_eq0 orbF. Qed. |