From 171c73b40b985f604e4d6c1529fb28d1dfa8e300 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Mar 2009 08:18:53 +0000
Subject: Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H
 at 4" now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
 etc.). The terminology for clauses (though I don't find the term "clause"
 very intuitive after all) is mostly preserved except for "simple_clause"
 which becomes a light form of "clause" instead of being an atom of clause
 (what played the role of "simple_clause" is now called "goal_location" -
 better names are welcome). Main changes are in tacticals.ml and tactics.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/pattern.v | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v
index 28d0bd556d..23e6f8e359 100644
--- a/test-suite/success/pattern.v
+++ b/test-suite/success/pattern.v
@@ -5,3 +5,40 @@
 
 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.
-- 
cgit v1.2.3