Commit 45b9c079 authored by Robbert Krebbers's avatar Robbert Krebbers


parent 22b68d48
......@@ -81,6 +81,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
* The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
* Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic.
* Make use of `ofe_iso` in the COFE solver.
* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
`{o,r,ur}Functor_apply` to better match their intent.
**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