Making parentheses mandatory in tactic scopes.

5 files changed, 15 insertions, 15 deletions

diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index aad0bb44d5..8dadc2419c 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -65,7 +65,7 @@ Module NonPrim.
     set (fibermap := fun a0p : hfiber f (f a)
                      => let (a0, p) := a0p in transport P p (d a0)).
     Set Printing Implicit.
-    let G := match goal with |- ?G => constr:G end in
+    let G := match goal with |- ?G => constr:(G) end in
     first [ match goal with
               | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                         (@isconnected_hfiber_conn_map n A B f H (f a))
@@ -142,7 +142,7 @@ Module Prim.
     set (fibermap := fun a0p : hfiber f (f a)
                      => let (a0, p) := a0p in transport P p (d a0)).
     Set Printing Implicit.
-    let G := match goal with |- ?G => constr:G end in
+    let G := match goal with |- ?G => constr:(G) end in
     first [ match goal with
               | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                         (@isconnected_hfiber_conn_map n A B f H (f a))
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index 070d1e9c71..a327bbf2a9 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -23,7 +23,7 @@ Proof.
   pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H
                                     (fun b => ap g (eisretr f b))) as k.
   revert k.
-  let x := match goal with |- let k := ?x in _ => constr:x end in
+  let x := match goal with |- let k := ?x in _ => constr:(x) end in
   intro k; clear k;
   pose (x _).
   pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index 52dae265bd..04fa59075b 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -39,7 +39,7 @@ Admitted.
 Ltac Zcst t :=
   match isZcst t with
     true => t
-  | _ => constr:NotConstant
+  | _ => constr:(NotConstant)
   end.
 
 Add Ring Zr : Zth
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index 7069bba430..8462d36272 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
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 6c4d4ae98f..ce90990594 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -15,7 +15,7 @@ Ltac F x := idtac; G x
  with G y := idtac; F y.
 
 (* Check that Match Context keeps a closure *)
-Ltac U := let a := constr:I in
+Ltac U := let a := constr:(I) in
           match goal with
           |  |- _ => apply a
           end.
@@ -75,7 +75,7 @@ Qed.
 
 (* Check context binding *)
 Ltac sym t :=
-  match constr:t with
+  match constr:(t) with
   | context C[(?X1 = ?X2)] => context C [X1 = X2]
   end.
 
@@ -143,7 +143,7 @@ Qed.
 
 Ltac check_binding y := cut ((fun y => y) = S).
 Goal True.
-check_binding ipattern:H.
+check_binding ipattern:(H).
 Abort.
 
 (* Check that variables explicitly parsed as ltac variables are not
@@ -151,7 +151,7 @@ Abort.
 
 Ltac afi tac := intros; tac.
 Goal 1 = 2.
-afi ltac:auto.
+afi ltac:(auto).
 Abort.
 
 (* Tactic Notation avec listes *)
@@ -174,7 +174,7 @@ Abort.
    empty args *)
 
 Goal True.
-match constr:@None with @None => exact I end.
+match constr:(@None) with @None => exact I end.
 Abort.
 
 (* Check second-order pattern unification *)
@@ -218,7 +218,7 @@ Ltac Z1 t := set (x:=t).
 Ltac Z2 t := t.
 Goal True -> True.
 Z1 O.
-Z2 ltac:O.
+Z2 ltac:(O).
 exact I.
 Qed.
 
@@ -302,7 +302,7 @@ Abort.
 (* Check instantiation of binders using ltac names *)
 
 Goal True.
-let x := ipattern:y in assert (forall x y, x = y + 0).
+let x := ipattern:(y) in assert (forall x y, x = y + 0).
 intro.
 destruct y. (* Check that the name is y here *)
 Abort.