diff options
| -rw-r--r-- | CHANGELOG.md | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 2 |
4 files changed, 6 insertions, 7 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md index 9fc7501..187d202 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,10 +10,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Changed - `eqVneq` lemma is changed from `{x = y} + {x != y}` to - `eq_xor_neq x y (y == x) (x == y)` which allows to use it as - a view like `eqP`, in addition providing simultaneous destruction - of expressions of the form `x == y` and `y == x`, while keeping - the ability to use it in a way it was used before. + `eq_xor_neq x y (y == x) (x == y)` which allows to use as a view and provide + simultaneous destruction of expressions of the form `x == y` and `y == x`, + while keeping the ability to use it in the way it was used before. ## [1.9.0] - 2019-05-22 diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 2ac2c3e..b65742d 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -2238,7 +2238,7 @@ Proof. apply/eqP/idP=> [d0|]; last first. case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|]. by move/divp_small. -case: (eqVneq p 0) => [->//|pn0]; case: (eqVneq q 0) => [->//| qn0]. +case: eqVneq => // _; case: eqVneq => // qn0. move: (divp_eq p q); rewrite d0 mul0r add0r. move/(f_equal (fun x : {poly R} => size x)). by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index dd14013..2e025a2 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -837,7 +837,7 @@ Qed. Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1). Proof. case: (eqsVneq G 1) => [-> |]; first by rewrite rank1. -case: (trivgVpdiv G) => [-> | [p p_pr]]; first by rewrite eqxx. +case: (trivgVpdiv G) => [/eqP->// | [p p_pr]]. case/Cauchy=> // x Gx oxp _; apply: leq_trans (p_rank_le_rank p G). have EpGx: <[x]>%G \in 'E_p(G). by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index e4e0003..7e1cdc8 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -201,7 +201,7 @@ Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set := | NeqNotEq of x != y : eq_xor_neq x y false false. Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y). -Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed. +Proof. by rewrite eq_sym; case: (altP eqP); constructor. Qed. Arguments eqVneq {T} x y, {T x y}. |