From a6d52d2502c09e8acdca464faf67d3956448cbcf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 27 Sep 2020 10:46:48 +0200
Subject: Prim.pattern_ident takes a location and its synonymous
 pattern_identref is deprecated.

---
 dev/doc/changes.md | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fb5d7cc244..8d0bcd1ee6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -17,6 +17,11 @@
   was instead intended. If cancelling the breaking role of cuts in the
   box was intended, turn `h n c` into `h c`.
 
+### Grammar entries
+
+- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident`
+  which now returns a located identifier.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
-- 
cgit v1.2.3