From f7004c56875ad0495a25cd1ff617b0f109b3b332 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Nov 2020 19:15:11 +0100
Subject: Removing non relevant argument binding_kind of GLocalDef.

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

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 5adeafaa38..26c4b01c9f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -37,6 +37,11 @@ Dumpglob:
   plugins to temporarily change/pause the output of Dumpglob, and then
   restore it to the original setting.
 
+Glob_term:
+
+- Removing useless `binding_kind` argument of `GLocalDef` in
+  `extended_glob_local_binder`.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
-- 
cgit v1.2.3