From 7050ceaa09a29c3f50620a8d3f8439c3d69a10d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Dec 2018 23:46:19 +0100
Subject: Documenting syntax "injection ... as [= pat1 ... patn ]".

To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
---
 doc/changelog/04-tactics/09288-injection-as.rst |  4 ++++
 doc/sphinx/proof-engine/tactics.rst             | 19 ++++++++++++++++---
 2 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 doc/changelog/04-tactics/09288-injection-as.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst
new file mode 100644
index 0000000000..6a74551f06
--- /dev/null
+++ b/doc/changelog/04-tactics/09288-injection-as.rst
@@ -0,0 +1,4 @@
+- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as
+  an alternative to :n:`injection @term as {+ @simple_intropattern}` using
+  the standard :n:`@injection_intropattern` syntax (`#09288
+  <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 67d32835f5..fa6d62ffa2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -131,16 +131,17 @@ include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`.
    simple_intropattern_closed : `naming_intropattern`
                               : _
                               : `or_and_intropattern`
-                              : `equality_intropattern`
+                              : `rewriting_intropattern`
+                              : `injection_intropattern`
    naming_intropattern     : `ident`
                            : ?
                            : ?`ident`
    or_and_intropattern     : [ `intropattern_list` | ... | `intropattern_list` ]
                            : ( `simple_intropattern` , ... , `simple_intropattern` )
                            : ( `simple_intropattern` & ... & `simple_intropattern` )
-   equality_intropattern   : ->
+   rewriting_intropattern  : ->
                            : <-
-                           : [= `intropattern_list` ]
+   injection_intropattern  : [= `intropattern_list` ]
    or_and_intropattern_loc : `or_and_intropattern`
                            : `ident`
 
@@ -2285,6 +2286,18 @@ and an explanation of the underlying technique.
       to the number of new equalities. The original equality is erased if it
       corresponds to a hypothesis.
 
+   .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern
+             injection @num as @injection_intropattern
+             injection as @injection_intropattern
+             einjection @term {? with @bindings_list} as @injection_intropattern
+             einjection @num as @injection_intropattern
+             einjection as @injection_intropattern
+
+      These are equivalent to the previous variants but using instead the
+      syntax :token:`injection_intropattern` which :tacn:`intros`
+      uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves
+      the same as :n:`as {+ @simple_intropattern}`.
+
    .. flag:: Structural Injection
 
       This option ensure that :n:`injection @term` erases the original hypothesis
-- 
cgit v1.2.3