Improving syntax of pat/constr introduction pattern so that

pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.

Open to other suggestions of syntax though.

3 files changed, 24 insertions, 6 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1551b8eefd..03c4f6a365 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -828,7 +828,9 @@ either:
     \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
     \item the rewriting orientations: {\tt ->} or {\tt <-}
     \end{itemize}
-  \item the on-the-fly application of a lemma: $p${\tt /{\term}}
+  \item the on-the-fly application of lemmas: $p${\tt /{\term$_1$}}
+    \ldots {\tt /{\term$_n$}} where $p$ itself is not an on-the-fly
+    application of lemmas pattern
   \end{itemize}
 \item the wildcard: {\tt \_}
 \end{itemize}
@@ -896,9 +898,10 @@ introduction pattern~$p$:
   itself is erased; if the term to substitute is a variable, it is
   substituted also in the context of goal and the variable is removed
   too;
-\item introduction over a pattern $p${\tt /{\term}} first applies
-  {\term} on the hypothesis to be introduced (as in {\tt apply
-  }{\term} {\tt in}), prior to the application of the introduction
+\item introduction over a pattern $p${\tt /{\term$_1$}} \ldots {\tt
+  /{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the
+  hypothesis to be introduced (as in {\tt apply }{\term}$_1$, \ldots,
+  {\term}$_n$ {\tt in}), prior to the application of the introduction
   pattern $p$;
 \item introduction on the wildcard depends on whether the product is
   dependent or not: in the non-dependent case, it erases the
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8e5e1f1fb8..b7559a1989 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -296,11 +296,17 @@ GEXTEND Gram
       | "**" -> !@loc, IntroForthcoming false ]]
   ;
   simple_intropattern:
+    [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] ->
+          let loc0,pat = pat in
+          let f c pat =
+            let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
+            IntroAction (IntroApplyOn (c,(loc,pat))) in
+          !@loc, List.fold_right f l pat ] ]
+  ;
+  simple_intropattern_closed:
     [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
       | pat = equality_intropattern -> !@loc, IntroAction pat
       | "_" -> !@loc, IntroAction IntroWildcard 
-      | pat = simple_intropattern; "/"; c = constr ->
-          !@loc, IntroAction (IntroApplyOn (c,pat))
       | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
   ;
   simple_binding:
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 35ba94fb67..741f372ff2 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -69,3 +69,12 @@ intros H (H1,?)/H.
 change (1=1) in H0.
 exact H1.
 Qed.
+
+(* Checking iterated pat/c1.../cn introduction patterns and side conditions *)
+
+Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
+intros * H H0 H1.
+intros H2/H/H0.
+- exact H2.
+- exact H1.
+Qed.