1 files changed, 42 insertions, 0 deletions
diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v
index 28d0bd55..72f84052 100644
--- a/test-suite/success/pattern.v
+++ b/test-suite/success/pattern.v
@@ -5,3 +5,45 @@
 
 Goal (id true,id false)=(id true,id true).
 generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff.
+Abort.
+
+(* Check use of occurrences in hypotheses for a reduction tactic such
+   as pattern *)
+
+(* Did not work in 8.2 *)
+Goal 0=0->True.
+intro H.
+pattern 0 in H at 2.
+set (f n := 0 = n) in H.  (* check pattern worked correctly *)
+Abort.
+
+(* Syntactic variant which was working in 8.2 *)
+Goal 0=0->True.
+intro H.
+pattern 0 at 2 in H.
+set (f n := 0 = n) in H.  (* check pattern worked correctly *)
+Abort.
+
+(* Ambiguous occurrence selection *)
+Goal 0=0->True.
+intro H.
+pattern 0 at 1 in H at 2 || exact I.  (* check pattern fails *)
+Qed.
+
+(* Ambiguous occurrence selection *)
+Goal 0=1->True.
+intro H.
+pattern 0, 1 in H at 1 2 || exact I.  (* check pattern fails *)
+Qed.
+
+(* Occurrence selection shared over hypotheses is difficult to advocate and
+   hence no longer allowed *)
+Goal 0=1->1=0->True.
+intros H1 H2.
+pattern 0 at 1, 1 in H1, H2 || exact I.  (* check pattern fails *)
+Qed.
+
+(* Test catching of reduction tactics errors (was not the case in 8.2) *)
+Goal eq_refl 0 = eq_refl 0.
+pattern 0 at 1 || reflexivity.
+Qed.