From 0f568166e37216a6e174e81757f6f2a2bc56fb4e Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 19 Dec 2019 13:40:36 +0100
Subject: Add changelog for non maximal implicit args

---
 .../02-specification-language/11235-non_maximal_implicit.rst        | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/11235-non_maximal_implicit.rst

diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
new file mode 100644
index 0000000000..aa42ef0fee
--- /dev/null
+++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Syntax for non maximal implicit arguments in toplevel definitions using
+  square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]``
+  to be consistent with the command :cmd:`Arguments (implicits)`.
+  (`#11235 <https://github.com/coq/coq/pull/11235>`_,
+  by SimonBoulier).
-- 
cgit v1.2.3