summaryrefslogtreecommitdiff
path: root/test-suite/success/MatchFail.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/MatchFail.v')
-rw-r--r--test-suite/success/MatchFail.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index 7069bba4..8462d362 100644
--- a/test-suite/success/MatchFail.v
+++ b/test-suite/success/MatchFail.v
@@ -9,14 +9,14 @@ Require Export ZArithRing.
Ltac compute_POS :=
match goal with
| |- context [(Zpos (xI ?X1))] =>
- let v := constr:X1 in
- match constr:v with
+ let v := constr:(X1) in
+ match constr:(v) with
| 1%positive => fail 1
| _ => rewrite (BinInt.Pos2Z.inj_xI v)
end
| |- context [(Zpos (xO ?X1))] =>
- let v := constr:X1 in
- match constr:v with
+ let v := constr:(X1) in
+ match constr:(v) with
| 1%positive => fail 1
| _ => rewrite (BinInt.Pos2Z.inj_xO v)
end