From cd5bb3c76e430392e4363dc7b4b5bbe0cafa466f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Feb 2020 23:28:04 +0100
Subject: Lately adding a changelog for PR#10202.

---
 .../10202-master+fix8011-stronger-check-on-typability-ltac-env.rst | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst

diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst
new file mode 100644
index 0000000000..57bce7e4f6
--- /dev/null
+++ b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst
@@ -0,0 +1,7 @@
+- **Changed:**
+  Warn when manual implicit arguments are used in unexpected positions
+  of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit
+  argument name is shadowed (e.g. in `Check fun f : forall {x:nat}
+  {x}, nat => f`)
+  (`#10202 <https://github.com/coq/coq/pull/10202>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3