blob: 55f44e68ced5cc4c52c05d8f4f6032138e0fe7dd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
# 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]
### Added
- Added fixpoint and cofixpoint constructions to `finset`: `fixset`,
`cofixset` and `fix_order`, with a few theorems about them
- Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their
"cancellation" lemmas.
- Added theorem `totient_prime` in `prime.v`
### 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.
|
