From fb124086cac13a53567ef8ec42f50128db136337 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 2 Apr 2020 13:29:49 +0200 Subject: [PATCH] CHANGELOG. --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a9da76d1e..6e00c253c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -91,6 +91,9 @@ Coq development, but not every API-breaking change is listed. Changes marked * 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. +* Affine, absorbing, persistent and timeless instances for telescopes. +* Better support for telescopes in the proof mode, i.e., all tactics should + recognize and distribute telescopes now. **Changes in heap_lang:** -- GitLab