Skip to content

Commit

Permalink
fix CHANGELOG (after rebase on top of PR math-comp#1136)
Browse files Browse the repository at this point in the history
  • Loading branch information
Tragicus committed Jan 17, 2024
1 parent db314ae commit 8be98d6
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@

- in `boolp.v`:
+ tactic `eqProp`
+ definition `BoolProp`
+ variant `BoolProp`
+ lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
`not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
`andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
Expand Down Expand Up @@ -312,9 +312,6 @@

### Changed

-in `boolp.v`
- lemmas `orC` and `andC` now use `commutative`

### Renamed

### Generalized
Expand Down

0 comments on commit 8be98d6

Please sign in to comment.