blob: 28264917b0455ac10a977e6caeaaa88c9321e19b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
# Changelog (unreleased)
To avoid having old PRs put changes into the wrong section of the CHANGELOG,
new entries now go to the present file as discussed
[here](https://github.com/math-comp/math-comp/wiki/Agenda-of-the-April-23rd-2019-meeting-9h30-to-12h30#avoiding-issues-with-changelog).
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
## [Unreleased]
### Changed
- `eqVneq` lemma is changed from `{x = y} + {x != y}` to
`eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs
simultaneous replacement of expressions of the form `x == y` and `y == x`
by `true` or `false`, while keeping the ability to use it in the way
it was used before.
|
