From dd7f79809425543b8ac3ff2c2a2b8f36adf28af1 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 6 Jan 2020 14:35:14 +0100
Subject: Non maximal implicits: entry in dev/doc/changes.md

---
 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 3bc92e6aee..cb6e695865 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -17,6 +17,11 @@ Printers:
   Constrextern.extern_constr which were taking a boolean argument for
   the goal style now take instead a label.
 
+Implicit arguments:
+
+- The type `Impargs.implicit_kind` was removed in favor of
+  `Glob_term.binding_kind`.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
-- 
cgit v1.2.3