Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.

Marking it as experimental.

7 files changed, 27 insertions, 23 deletions

diff --git a/CHANGES b/CHANGES
index 70ed1bef0..389572014 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,9 @@ Tactics
 
 - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
   for induction.
+- Syntax "p/c" for on-the-fly application of a lemma c before
+  introducing along pattern p changed to p%c1..%cn. The feature and
+  syntax are in experimental stage.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f367f04c4..3a3877105 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -813,7 +813,7 @@ either:
   \item the pattern \texttt{?\ident}
   \item an identifier
   \end{itemize}
-\item a {\em destructing introduction pattern} which itself classifies into:
+\item an {\em action introduction pattern} which itself classifies into:
   \begin{itemize}
   \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
     \begin{itemize}
@@ -828,9 +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 lemmas: $p${\tt /{\term$_1$}}
-    \ldots {\tt /{\term$_n$}} where $p$ itself is not an on-the-fly
-    application of lemmas pattern
+  \item the on-the-fly application of lemmas: $p${\tt \%{\term$_1$}}
+    \ldots {\tt \%{\term$_n$}} where $p$ itself is not a pattern for
+    on-the-fly application of lemmas (note: syntax is in experimental stage)
   \end{itemize}
 \item the wildcard: {\tt \_}
 \end{itemize}
@@ -898,10 +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$_1$}} \ldots {\tt
-  /{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the
+\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
+  {\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 4d42dfe85..3d59b9b8d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -311,7 +311,8 @@ GEXTEND Gram
       | "**" -> !@loc, IntroForthcoming false ]]
   ;
   simple_intropattern:
-    [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] ->
+    [ [ pat = simple_intropattern_closed;
+        l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
           let loc0,pat = pat in
           let f c pat =
             let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 741f372ff..17f160f98 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -34,47 +34,47 @@ intros _ ?.
 exact H.
 Qed.
 
-(* A short test about introduction pattern pat/c *)
+(* A short test about introduction pattern pat%c *)
 Goal (True -> 0=0) -> True /\ False -> 0=0.
-intros H (H1/H,_).
+intros H (H1%H,_).
 exact H1.
 Qed.
 
 (* A test about bugs in 8.5beta2 *)
 Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
 intros H H0 H1.
-destruct H0 as (a/H,_).
+destruct H0 as (a%H,_).
 (* Check that H0 is removed (was bugged in 8.5beta2) *)
 Fail clear H0.
-(* Check position of newly created hypotheses when using pat/c (was
+(* Check position of newly created hypotheses when using pat%c (was
    left at top in 8.5beta2) *)
 match goal with H:_ |- _ => clear H end. (* clear H1:False *)
 match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
 Qed.
 
 Goal (True -> 0=0) -> True -> 0=0.
-intros H H1/H.
+intros H H1%H.
 exact H1.
 Qed.
 
 Goal forall n, n = S n -> 0=0.
-intros n H/n_Sn.
+intros n H%n_Sn.
 destruct H.
 Qed.
 
 (* Another check about generated names and cleared hypotheses with
-   pat/c patterns *)
+   pat%c patterns *)
 Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
-intros H (H1,?)/H.
+intros H (H1,?)%H.
 change (1=1) in H0.
 exact H1.
 Qed.
 
-(* Checking iterated pat/c1.../cn introduction patterns and side conditions *)
+(* 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.
+intros H2%H%H0.
 - exact H2.
 - exact H1.
 Qed.
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
index 408eca4a3..abe6a8d99 100644
--- a/theories/Logic/WKL.v
+++ b/theories/Logic/WKL.v
@@ -40,7 +40,7 @@ Proposition is_path_from_characterization P n l :
 Proof.
 intros. split.
 - induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')].
-  + exists []. split. reflexivity. intros n <-/le_n_0_eq. assumption.
+  + exists []. split. reflexivity. intros n <-%le_n_0_eq. assumption.
   + exists (true :: l'). split. apply eq_S, Hl'. intros [|] H.
     * assumption.
     * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H.
@@ -51,10 +51,10 @@ intros. split.
   + constructor. apply (HPl' 0). apply le_0_n.
   + eapply next_left.
     * apply (HPl' 0), le_0_n.
-    * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+    * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
   + apply next_right.
     * apply (HPl' 0), le_0_n.
-    * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+    * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
 Qed.
 
 (** [infinite_from P l] means that we can find arbitrary long paths
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
index 2f84ebe5f..365661be0 100644
--- a/theories/Logic/WeakFan.v
+++ b/theories/Logic/WeakFan.v
@@ -89,7 +89,7 @@ Qed.
 Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
 Proof.
 intros P Hbar.
-destruct Hbar with (X P) as (l,(Hd/Y_approx,HP)).
+destruct Hbar with (X P) as (l,(Hd%Y_approx,HP)).
 assert (inductively_barred P l) by (apply (now P l), HP).
 clear Hbar HP.
 induction l as [|a l].
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index dd9e4c986..b8b9e929c 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -95,7 +95,7 @@ Section Wf_Lexicographic_Exponentiation.
      intros.
     - inversion H.
       assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets.
-      destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)/app_inj_tail, <-).
+      destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-).
       inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ].
     - inversion H0.
       + apply app_cons_not_nil in H3 as ().