From 42c191a8fd8624b80be77433e972e259397fd734 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 1 Apr 2020 00:23:17 +0200 Subject: [PATCH] CHANGELOG. --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c8934aea5..a9da76d1e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -88,6 +88,9 @@ Coq development, but not every API-breaking change is listed. Changes marked `inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q` and (similar for `na_inv_iff` and `cinv_iff`), following e.g., `inv_alter` and `wp_wand`. * Add lemma `is_lock_iff` and show that `is_lock` is contractive. +* Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into + `{o,r,ur}Functor_map_{ne,id,compose,contractive}`. +* Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors. **Changes in heap_lang:** -- GitLab