Merge PR #11317: Fix #11140: Bidirectionality hints perform (surprising?) simplification

Reviewed-by: SkySkimmer
Ack-by: gares
Reviewed-by: mattam82

3 files changed, 18 insertions, 13 deletions

diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst
new file mode 100644
index 0000000000..8c84648aa7
--- /dev/null
+++ b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst
@@ -0,0 +1,4 @@
+- **Fixed:** `#11360 <https://github.com/issues/11360>`_
+  Broken section closing when a template polymorphic inductive type depends on
+  a section variable through its parameters (`#11361
+  <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78428be18f..8d59e64cdb 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2547,3 +2547,8 @@ the context to help inferring the types of the remaining arguments.
 
       Arguments ex_intro _ _ & _ _.
       Check (ex_intro _ true _ : exists n : nat, n > 0).
+
+Coq will attempt to produce a term which uses the arguments you
+provided, but in some cases involving Program mode the arguments after
+the bidirectionality starts may be replaced by convertible but
+syntactically different terms.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 368724f9d2..70dadedd35 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -327,11 +327,8 @@ function on type :g:`A`). The keyword :g:`fun` can be followed by several
 binders as given in Section :ref:`binders`. Functions over
 several variables are equivalent to an iteration of one-variable
 functions. For instance the expression
-“fun :token:`ident`\ :math:`_{1}` … :token:`ident`\ :math:`_{n}` 
-: :token:`type` => :token:`term`”
-denotes the same function as “ fun :token:`ident`\
-:math:`_{1}` : :token:`type` => … 
-fun :token:`ident`\ :math:`_{n}` : :token:`type` => :token:`term`”. If
+:n:`fun {+ @ident__i } : @type => @term`
+denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If
 a let-binder occurs in
 the list of binders, it is expanded to a let-in definition (see
 Section :ref:`let-in`).
@@ -362,15 +359,14 @@ the propositional implication and function types.
 Applications
 ------------
 
-The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` denotes the
-application of :token:`term`\ :math:`_0` to :token:`term`\ :math:`_1`.
+The expression :n:`@term__fun @term` denotes the application of
+:n:`@term__fun` (which is expected to have a function type) to
+:token:`term`.
 
-The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ...
-:token:`term`\ :math:`_n` denotes the application of the term
-:token:`term`\ :math:`_0` to the arguments :token:`term`\ :math:`_1` ... then
-:token:`term`\ :math:`_n`. It is equivalent to ( … ( :token:`term`\ :math:`_0`
-:token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the
-left.
+The expression :n:`@term__fun {+ @term__i }` denotes the application
+of the term :n:`@term__fun` to the arguments :n:`@term__i`.  It is
+equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`:
+associativity is to the left.
 
 The notation :n:`(@ident := @term)` for arguments is used for making
 explicit the value of implicit arguments (see