Commit fb124086 authored by Robbert Krebbers's avatar Robbert Krebbers


parent 50ba690d
......@@ -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
* 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:**
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment