blob: 1892bcac7c48f810ed959bda3fb4db940d92b308 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
# 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)` 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.
|
