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

---
 doc/changelog/02-specification-language/11235-non_maximal_implicit.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
index aa42ef0fee..d8ff1fec31 100644
--- a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
+++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
@@ -1,5 +1,5 @@
 - **Added:**
-  Syntax for non maximal implicit arguments in toplevel definitions using
+  Syntax for non maximal implicit arguments in definitions and terms 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>`_,
-- 
cgit v1.2.3