Skip to content

Commit

Permalink
changelog
Browse files Browse the repository at this point in the history
  • Loading branch information
Tragicus committed Aug 6, 2024
1 parent 94b3b7b commit dcdaf49
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,9 @@
- moved from `lebesgue_integral.v` to `cardinality.v`:
+ hint `solve [apply: fimfunP]`

- in `mathcomp_extra.v`:
+ Notation "f \^-1" now at level 35 with f at next level

### Renamed

- in `constructive_ereal.v`:
Expand Down

0 comments on commit dcdaf49

Please sign in to comment.