Skip to content

Commit

Permalink
undo eq_lt_total and le_lt_total
Browse files Browse the repository at this point in the history
  • Loading branch information
@t6s @affeldt-aist
t6s authored and affeldt-aist committed Jan 7, 2025
1 parent 46c9399 commit b21ee0c
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions CHANGELOG_UNRELEASED.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,6 @@

### Added

- in file `mathcomp_extra.v`,
+ lemmas `eq_lt_total`, `le_lt_total`

- file `Rstruct_topology.v`

- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`
Expand Down

0 comments on commit b21ee0c

Please sign in to comment.