diff --git a/CHANGELOG.md b/CHANGELOG.md index edf2268c4a30ab695e80c4593351411d265fbd28..8ddd564983da5867b47301aa8196871931b7f102 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ Coq development, but not every API-breaking change is listed. Changes marked **Changes in Coq:** +* Added support for Coq 8.10; dropped support for Coq 8.7. * A new tactic `iStopProof` to turn the proof mode entailment into an ordinary Coq goal `big star of context ⊢ proof mode goal`. * Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.