From d2339d53275a887a037d182d5e952689e68b2432 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 May 2019 19:48:34 +0200
Subject: [PATCH] Markdown tweak.
---
CHANGELOG.md | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6815004e8..fa3956dff 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,11 +53,10 @@ Changes in Coq:
- `iModIntro` is more flexible and more powerful, it now also subsumes
`iNext` and `iAlways`.
- General infrastructure for deriving a logic for monotone predicates over
- an existing logic (see the paper for more details).
-
+ an existing logic (see the paper for more details).
Developments instantiating the proof mode typeclasses may need significant
- changes. For developments just using the proof mode tactics, porting should
- not be too much effort. Notable things to port are:
+ changes. For developments just using the proof mode tactics, porting should
+ not be too much effort. Notable things to port are:
- All the BI laws moved from the `uPred` module to the `bi` module. For
example, `uPred.later_equivI` became `bi.later_equivI`.
- Big-ops are automatically imported, imports of `iris.base_logic.big_op` have
--
GitLab