From 34c6885b72167d8b4ecb91c537206c02512d11c7 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 8 Jan 2024 15:12:26 +0100 Subject: [PATCH] fix CHANGELOG (after rebase on top of PR #1136) --- CHANGELOG_UNRELEASED.md | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f62e89d37b..399547f181 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -134,7 +134,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`, @@ -267,16 +267,6 @@ `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`, `absurd : { hyp_list(Hs) } ident(H)` - -- in `boolp.v`: - + tactic `eqProp` - + 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`, - `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`, - `inhabitedE`, `inhabited_witness` - ### Changed - in `normedtype.v`: @@ -318,9 +308,6 @@ -in `boolp.v` - lemmas `orC` and `andC` now use `commutative` --in `boolp.v` - - lemmas `orC` and `andC` now use `commutative` - ### Renamed - in `exp.v`: