diff --git a/CHANGELOG.md b/CHANGELOG.md index 98c97a38422f23fa6b8b1f4f4073d5a6044b1b72..bc5c7dbf2d6302d324f7efbc0d5bc77a5e348cbe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,7 +5,7 @@ Coq development, but not every API-breaking change is listed. Changes marked ## Iris 3.0 -# Lifting lemmas do no longer take as hypothesis the fact the the +* [#] Lifting lemmas do no longer take as hypothesis the fact the the considered expression is not a value. This is deduced from the fact that it is reducible. * View shifts are radically simplified to just internalize frame-preserving