This example does not work in coq-7.3, but does in coq-7.2.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2766 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
new file mode 100644
index 000000000..a62113d12
--- /dev/null
+++ b/test-suite/success/MatchFail.v
@@ -0,0 +1,23 @@
+Require Export ZArith.
+Require Export ZArithRing.
+
+Tactic Definition compute_POS :=
+ (Match Context With
+ | [|- [(POS (xI ?1))]] -> Let v = ?1 In 
+                          (Match v With
+                            | [xH] ->
+                              (Fail 1)
+                            |_->
+                              Rewrite (POS_xI v))
+ | [ |- [(POS (xO ?1))]] -> Let v = ?1 In
+                           Match v With
+                            |[xH]->
+                              (Fail 1)
+                            |[?]->
+                              Rewrite (POS_xO v)).
+
+Goal (x:positive)(POS (xI (xI x)))=`4*(POS x)+3`.
+Intros.
+Repeat compute_POS.
+Ring.
+Qed.