Merge PR #12246: Adding support for applying in several hypotheses at the same time (granting #9816)

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 20 insertions, 15 deletions

diff --git a/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst b/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst
new file mode 100644
index 0000000000..15ab18dcf1
--- /dev/null
+++ b/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  `apply in` supports several hypotheses
+  (`#12246 <https://github.com/coq/coq/pull/12246>`_,
+  by Hugo Herbelin; grants
+  `#9816 <https://github.com/coq/coq/pull/9816>`_).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 26a56005c1..4f01559cad 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -878,38 +878,38 @@ Applying theorems
       This happens if the conclusion of :token:`ident` does not match any of
       the non-dependent premises of the type of :token:`term`.
 
-   .. tacv:: apply {+, @term} in @ident
+   .. tacv:: apply {+, @term} in {+, @ident}
 
-      This applies each :token:`term` in sequence in :token:`ident`.
+      This applies each :token:`term` in sequence in each hypothesis :token:`ident`.
 
-   .. tacv:: apply {+, @term with @bindings} in @ident
+   .. tacv:: apply {+, @term with @bindings} in {+, @ident}
 
-      This does the same but uses the bindings in each :n:`(@ident := @term)` to
-      instantiate the parameters of the corresponding type of :token:`term`
-      (see :ref:`bindings`).
+      This does the same but uses the bindings to instantiate
+      parameters of :token:`term` (see :ref:`bindings`).
 
-   .. tacv:: eapply {+, @term {? with @bindings } } in @ident
+   .. tacv:: eapply {+, @term {? with @bindings } } in {+, @ident}
 
       This works as :tacn:`apply … in` but turns unresolved bindings into
       existential variables, if any, instead of failing.
 
-   .. tacv:: apply {+, @term {? with @bindings } } in @ident as @simple_intropattern
+   .. tacv:: apply {+, @term {? with @bindings } } in {+, @ident {? as @simple_intropattern}}
       :name: apply … in … as
 
-      This works as :tacn:`apply … in` then applies the :token:`simple_intropattern`
-      to the hypothesis :token:`ident`.
+      This works as :tacn:`apply … in` but applying an associated
+      :token:`simple_intropattern` to each hypothesis :token:`ident`
+      that comes with such clause.
 
-   .. tacv:: simple apply @term in @ident
+   .. tacv:: simple apply @term in {+, @ident}
 
       This behaves like :tacn:`apply … in` but it reasons modulo conversion
       only on subterms that contain no variables to instantiate and does not
       traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`.
 
-   .. tacv:: {? simple} apply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
-             {? simple} eapply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
+   .. tacv:: {? simple} apply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}}
+             {? simple} eapply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}}
 
-      This summarizes the different syntactic variants of :n:`apply @term in @ident`
-      and :n:`eapply @term in @ident`.
+      This summarizes the different syntactic variants of :n:`apply @term in {+, @ident}`
+      and :n:`eapply @term in {+, @ident}`.
 
 .. tacn:: constructor @natural
    :name: constructor