Imported Upstream version 8.6upstream/8.6

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