From 090cdbf9dc19d5c84cbeaf0d6663ad24e5a00965 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 6 Apr 2020 09:46:43 -0500
Subject: [PATCH] Reword directing to iris/string-ident

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b55e59c9f..88c6ce1e6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -103,9 +103,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   + `singleton_included_exclusive` → `singleton_included_exclusive_l`
 * The proof mode now supports names for pure facts in intro patterns. Support
   requires implementing `string_to_ident`. Without this tactic such patterns
-  will fail. We provide one implementation at
-  https://gitlab.mpi-sws.org/iris/string-ident using Ltac2 which works with Coq
-  8.11 and can be installed with opam (see the README for details).
+  will fail. We provide one implementation using Ltac2 which works with Coq 8.11
+  and can be installed with opam; see
+  [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
 
 **Changes in heap_lang:**
 
-- 
GitLab