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

Marking it as experimental.

3 files changed, 5 insertions, 5 deletions

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 ().