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.

8 files changed, 56 insertions, 10 deletions

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
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index f5098d2a34..4c186dce09 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -146,6 +146,23 @@ let discrHyp id =
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None None) with_evars c
 
+let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None
+
+let decode_inj_ipat ?loc = function
+  (* For the "as [= pat1 ... patn ]" syntax *)
+  | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat
+  (* For the "as pat1 ... patn" syntax *)
+  | ([] | [_]) as ipat -> ipat
+  | pat1::pat2::_ as ipat ->
+  (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs
+     in the non-singleton list of patterns *)
+  match isInjPat pat1 with
+  | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.")
+  | None ->
+  match List.map_filter isInjPat ipat with
+  | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.")
+  | [] -> ipat
+
 }
 
 TACTIC EXTEND injection
@@ -158,15 +175,15 @@ TACTIC EXTEND einjection
 END
 TACTIC EXTEND injection_as
 | [ "injection" "as" intropattern_list(ipat)] ->
-    { injClause None (Some ipat) false None }
+    { injClause None (Some (decode_inj_ipat ipat)) false None }
 | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    { mytclWithHoles (injClause None (Some ipat)) false c }
+    { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c }
 END
 TACTIC EXTEND einjection_as
 | [ "einjection" "as" intropattern_list(ipat)] ->
-    { injClause None (Some ipat) true None }
+    { injClause None (Some (decode_inj_ipat ipat)) true None }
 | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    { mytclWithHoles (injClause None (Some ipat)) true c }
+    { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c }
 END
 TACTIC EXTEND simple_injection
 | [ "simple" "injection" ] -> { simpleInjClause None false None }
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 36ed0210e3..b20f45af3e 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -925,7 +925,7 @@ Qed.
  revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
  - discriminate.
  - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
-   * injection H as <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 4886c8b9aa..9be2535a3f 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -105,7 +105,7 @@ Section ZMORPHISM.
  Proof.
   constructor.
   destruct c;intros;try discriminate.
-  injection H as <-.
+  injection H as [= <-].
   simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index f7cb6b688b..c5d396427b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -894,7 +894,7 @@ Section MakeRingPol.
  revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
  - discriminate.
  - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
-   * injection H as <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/test-suite/output/injection.out b/test-suite/output/injection.out
new file mode 100644
index 0000000000..ff40a478f3
--- /dev/null
+++ b/test-suite/output/injection.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Unexpected pattern.
+The command has indeed failed with message:
+Unexpected injection pattern.
diff --git a/test-suite/output/injection.v b/test-suite/output/injection.v
new file mode 100644
index 0000000000..bfd5a67bf5
--- /dev/null
+++ b/test-suite/output/injection.v
@@ -0,0 +1,8 @@
+(* Test error messages *)
+
+Goal forall x, (x,0) = (0, S x) -> x = 0.
+Fail intros x H; injection H as [= H'] H''.
+Fail intros x H; injection H as H' [= H''].
+intros x H; injection H as [= H' H''].
+exact H'.
+Qed.