Merge remote-tracking branch 'origin/master' into stm+doc_hook

2 files changed, 40 insertions, 27 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 418922e9b3..3a12ee288a 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme``
 Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
 
-.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort
+.. cmd:: Derive Inversion @ident with @ident Sort @sort
+         Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort
 
    This command generates an inversion principle for the
-   :tacn:`inversion ... using ...`  tactic. Let :g:`I` be an inductive
-   predicate and :g:`x` the variables occurring in t. This command
-   generates and stocks the inversion lemma for the sort :g:`sort`
-   corresponding to the instance :g:`∀ (x:T), I t` with the name
-   :n:`@ident` in the global environment. When applied, it is
-   equivalent to having inverted the instance with the tactic
-   :g:`inversion`.
-
+   :tacn:`inversion ... using ...` tactic.  The first :token:`ident` is the name
+   of the generated principle.  The second :token:`ident` should be an inductive
+   predicate, and :token:`binders` the variables occurring in the term
+   :token:`term`. This command generates the inversion lemma for the sort
+   :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`.
+   When applied, it is equivalent to having inverted the instance with the
+   tactic :g:`inversion`.
 
-.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
+          Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with the
    tactic inversion replaced by the tactic `inversion_clear`.
 
-.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort
+          Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
-.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort
+          Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3ca1dda4d6..cda228a7da 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -327,22 +327,29 @@ symbols.
 Reserving notations
 ~~~~~~~~~~~~~~~~~~~
 
-A given notation may be used in different contexts. Coq expects all
-uses of the notation to be defined at the same precedence and with the
-same associativity. To avoid giving the precedence and associativity
-every time, it is possible to declare a parsing rule in advance
-without giving its interpretation. Here is an example from the initial
-state of Coq.
+.. cmd:: Reserved Notation @string {? (@modifiers) }
 
-.. coqtop:: in
+   A given notation may be used in different contexts. Coq expects all
+   uses of the notation to be defined at the same precedence and with the
+   same associativity. To avoid giving the precedence and associativity
+   every time, this command declares a parsing rule (:token:`string`) in advance
+   without giving its interpretation. Here is an example from the initial
+   state of Coq.
+
+   .. coqtop:: in
 
-   Reserved Notation "x = y" (at level 70, no associativity).
+      Reserved Notation "x = y" (at level 70, no associativity).
 
-Reserving a notation is also useful for simultaneously defining an
-inductive type or a recursive constant and a notation for it.
+   Reserving a notation is also useful for simultaneously defining an
+   inductive type or a recursive constant and a notation for it.
 
-.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
-          their precedence and associativity cannot be changed.
+   .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
+             their precedence and associativity cannot be changed.
+
+   .. cmdv:: Reserved Infix "@symbol" {* @modifiers}
+
+      This command declares an infix parsing rule without giving its
+      interpretation.
 
 Simultaneous definition of terms and notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -840,10 +847,11 @@ gives a way to let any arbitrary expression which is not handled by the
 custom entry ``expr`` be parsed or printed by the main grammar of term
 up to the insertion of a pair of curly brackets.
 
-.. cmd:: Print Grammar @ident.
+.. cmd:: Print Custom Grammar @ident.
+   :name: Print Custom Grammar
 
-   This displays the state of the grammar for terms and grammar for
-   patterns associated to the custom entry :token:`ident`.
+   This displays the state of the grammar for terms associated to
+   the custom entry :token:`ident`.
 
 Summary
 ~~~~~~~
@@ -1376,6 +1384,8 @@ Abbreviations
    denoted expression is performed at definition time. Type checking is
    done only at the time of use of the abbreviation.
 
+.. _numeral-notations:
+
 Numeral notations
 -----------------