Merge PR #11509: Add changelog and fixes for #10202

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

2 files changed, 45 insertions, 0 deletions

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).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index b3ebb4d8df..7b4b652a6a 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1669,6 +1669,44 @@ For example:
 One can always specify the parameter if it is not uniform using the
 usual implicit arguments disambiguation syntax.
 
+The syntax is also supported in internal binders. For instance, in the
+following kinds of expressions, the type of each declaration present
+in :token:`binders` can be bracketed to mark the declaration as
+implicit:
+:n:`fun (@ident:forall @binders, @type) => @term`,
+:n:`forall (@ident:forall @binders, @type), @type`,
+:n:`let @ident @binders := @term in @term`,
+:n:`fix @ident @binders := @term in @term` and
+:n:`cofix @ident @binders := @term in @term`.
+Here is an example:
+
+.. coqtop:: all
+
+   Axiom Ax :
+     forall (f:forall {A} (a:A), A * A),
+     let g {A} (x y:A) := (x,y) in
+     f 0 = g 0 0.
+
+.. warn:: Ignoring implicit binder declaration in unexpected position
+
+   This is triggered when setting an argument implicit in an
+   expression which does not correspond to the type of an assumption
+   or to the body of a definition. Here is an example:
+
+   .. coqtop:: all warn
+
+      Definition f := forall {y}, y = 0.
+
+.. warn:: Making shadowed name of implicit argument accessible by position
+
+   This is triggered when two variables of same name are set implicit
+   in the same block of binders, in which case the first occurrence is
+   considered to be unnamed. Here is an example:
+
+   .. coqtop:: all warn
+
+      Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0.
+
 
 Declaring Implicit Arguments
 ++++++++++++++++++++++++++++