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.

4 files changed, 24 insertions, 7 deletions

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.