From 7e33ffcb5b25f81d7eaca9afabc7f928311bf5da Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 6 Apr 2020 09:20:01 -0500
Subject: [PATCH] Remove mention of string ident plugin

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 455986f07..617715a45 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -102,9 +102,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   + `singleton_included` → `singleton_included_l`.
   + `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` with either a plugin or Ltac2, which
-  only work on Coq 8.10 and Coq 8.11 respectively. Without this tactic such
-  patterns will fail.
+  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. See the [README](https://gitlab.mpi-sws.org/iris/string-ident) for opam
+  installation instructions.
 
 **Changes in heap_lang:**
 
-- 
GitLab