Commit bc17fc9e authored by Ralf Jung's avatar Ralf Jung

mention Coq 8.11 in changelog

parent 77852d7f
Pipeline #24184 passed with stage
in 16 minutes and 21 seconds
...@@ -20,7 +20,7 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -20,7 +20,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
**Changes in Coq:** **Changes in Coq:**
* Added support for Coq 8.10; dropped support for Coq 8.7. * Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7.
* A new tactic `iStopProof` to turn the proof mode entailment into an ordinary * A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
Coq goal `big star of context ⊢ proof mode goal`. Coq goal `big star of context ⊢ proof mode goal`.
* Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s. * Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.
......
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