From e7bfdf129e02a67bbe54794a6044239a7dc17c02 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Dec 2020 19:10:25 +0100
Subject: [PATCH] Better links in CHANGELOG.

---
 CHANGELOG.md | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cc6beab60..fdacba5fe 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -155,11 +155,12 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
     persistent proposition provides read-only access to `l`.
   + The lemma `mapsto_persist : l ↦{dq} v ==∗ l ↦□ v` is used for making the
     location `l` read-only.
-  + See the changes to HeapLang for an indication on how to adapt your language.
-  + See the changes to iris-examples for an indication on how to adapt your
-    development. In particular, instead of `∃ q, l ↦{q} v` you likely want to
-    use `l ↦□ v`, which has the advantage of being persistent (rather than just
-    duplicable).
+  + See the [changes to HeapLang](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/554)
+    for an indication on how to adapt your language.
+  + See the [changes to iris-examples](https://gitlab.mpi-sws.org/iris/examples/-/commit/a8425b708ec51d918d5cf6eb3ab6fde88f4e2c2a)
+    for an indication on how to adapt your development. In particular, instead
+    of `∃ q, l ↦{q} v` you likely want to use `l ↦□ v`, which has the advantage
+    of being persistent (rather than just duplicable).
 
 **Changes in `program_logic`:**
 
-- 
GitLab