Making parentheses mandatory in tactic scopes.

26 files changed, 170 insertions, 168 deletions

diff --git a/CHANGES b/CHANGES
index e80a3b454..ae055cb2f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,6 +13,8 @@ Tactics
 - In introduction patterns of the form (pat1,...,patn), n should match
   the exact number of hypotheses introduced (except for local definitions
   for which pattern can be omitted, as in regular pattern-matching).
+- Tactic scopes in Ltac like constr: and ltac: now require parentheses around
+  their argument.
 
 Program
 
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 45d2a09e7..b76f5dda2 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -146,11 +146,11 @@ GEXTEND Gram
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
   tactic_top_or_arg:
-    [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c
-      | IDENT "constr"; ":"; c = Constr.constr -> ConstrMayEval (ConstrTerm c)
-      | IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
-      | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n)
-      | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
+    [ [ IDENT "uconstr"; ":"; "("; c = Constr.lconstr; ")" -> UConstr c
+      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> ConstrMayEval (ConstrTerm c)
+      | IDENT "ltac"; ":"; "("; a = tactic_expr LEVEL "5"; ")" -> arg_of_expr a
+      | IDENT "ltac"; ":"; "("; n = natural; ")" -> TacGeneric (genarg_of_int n)
+      | IDENT "ipattern"; ":"; "("; ipat = simple_intropattern; ")" ->
         TacGeneric (genarg_of_ipattern ipat)
       | c = constr_eval -> ConstrMayEval c
       | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 50e0033e5..ba1f8956e 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -69,7 +69,7 @@ Ltac xpsatz dom d :=
   end in tac.
 
 Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
-Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
 
 Ltac psatzl dom :=
   let tac := lazymatch dom with
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b84cf2540..36511386a 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1492,7 +1492,7 @@ with Simplify := match goal with
   end.
 
 Ltac prove_stable x th :=
-  match constr:x with
+  match constr:(x) with
   | ?X1 =>
       unfold term_stable, X1; intros; Simplify; simpl;
        apply th
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 04decbce1..5f5b97925 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -32,13 +32,13 @@ Qed.
 Ltac natcst t :=
   match isnatcst t with
     true => constr:(N.of_nat t)
-  | _ => constr:InitialRing.NotConstant
+  | _ => constr:(InitialRing.NotConstant)
   end.
 
 Ltac Ss_to_add f acc :=
   match f with
   | S ?f1 => Ss_to_add f1 (S acc)
-  | _ => constr:(acc + f)%nat
+  | _ => constr:((acc + f)%nat)
   end.
 
 Ltac natprering :=
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 8362c8c26..8fcc07716 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -612,32 +612,32 @@ End GEN_DIV.
  Ltac inv_gen_phi_pos rI add mul t :=
    let rec inv_cst t :=
    match t with
-     rI => constr:1%positive
-   | (add rI rI) => constr:2%positive
-   | (add rI (add rI rI)) => constr:3%positive
+     rI => constr:(1%positive)
+   | (add rI rI) => constr:(2%positive)
+   | (add rI (add rI rI)) => constr:(3%positive)
    | (mul (add rI rI) ?p) => (* 2p *)
        match inv_cst p with
-         NotConstant => constr:NotConstant
-       | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *)
+         NotConstant => constr:(NotConstant)
+       | 1%positive => constr:(NotConstant) (* 2*1 is not convertible to 2 *)
        | ?p => constr:(xO p)
        end
    | (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
        match inv_cst p with
-         NotConstant => constr:NotConstant
-       | 1%positive => constr:NotConstant
+         NotConstant => constr:(NotConstant)
+       | 1%positive => constr:(NotConstant)
        | ?p => constr:(xI p)
        end
-   | _ => constr:NotConstant
+   | _ => constr:(NotConstant)
    end in
    inv_cst t.
 
 (* The (partial) inverse of gen_phiNword *)
  Ltac inv_gen_phiNword rO rI add mul opp t :=
    match t with
-     rO => constr:NwO
+     rO => constr:(NwO)
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Npos p::nil)
      end
    end.
@@ -646,10 +646,10 @@ End GEN_DIV.
 (* The inverse of gen_phiN *)
  Ltac inv_gen_phiN rO rI add mul t :=
    match t with
-     rO => constr:0%N
+     rO => constr:(0%N)
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Npos p)
      end
    end.
@@ -657,15 +657,15 @@ End GEN_DIV.
 (* The inverse of gen_phiZ *)
  Ltac inv_gen_phiZ rO rI add mul opp t :=
    match t with
-     rO => constr:0%Z
+     rO => constr:(0%Z)
    | (opp ?p) =>
      match inv_gen_phi_pos rI add mul p with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Zneg p)
      end
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:NotConstant
+       NotConstant => constr:(NotConstant)
      | ?p => constr:(Zpos p)
      end
    end.
@@ -681,7 +681,7 @@ Ltac inv_gen_phi rO rI cO cI t :=
   end.
 
 (* A simple tactic recognizing no constant *)
- Ltac inv_morph_nothing t := constr:NotConstant.
+ Ltac inv_morph_nothing t := constr:(NotConstant).
 
 Ltac coerce_to_almost_ring set ext rspec :=
   match type of rspec with
@@ -825,31 +825,31 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
 (* Tactic for constant *)
 Ltac isnatcst t :=
   match t with
-    O => constr:true
+    O => constr:(true)
   | S ?p => isnatcst p
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 Ltac isPcst t :=
   match t with
   | xI ?p => isPcst p
   | xO ?p => isPcst p
-  | xH => constr:true
+  | xH => constr:(true)
   (* nat -> positive *)
   | Pos.of_succ_nat ?n => isnatcst n
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 Ltac isNcst t :=
   match t with
-    N0 => constr:true
+    N0 => constr:(true)
   | Npos ?p => isPcst p
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 Ltac isZcst t :=
   match t with
-    Z0 => constr:true
+    Z0 => constr:(true)
   | Zpos ?p => isPcst p
   | Zneg ?p => isPcst p
   (* injection nat -> Z *)
@@ -857,7 +857,7 @@ Ltac isZcst t :=
   (* injection N -> Z *)
   | Z.of_N ?n => isNcst n
   (* *)
-  | _ => constr:false
+  | _ => constr:(false)
   end.
 
 
diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 6c1a79e4e..54e2789ba 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -15,7 +15,7 @@ Set Implicit Arguments.
 Ltac Ncst t :=
   match isNcst t with
     true => t
-  | _ => constr:NotConstant
+  | _ => constr:(NotConstant)
   end.
 
 Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]).
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index a0844100c..77576cb93 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -36,9 +36,9 @@ Qed.
 Ltac bool_cst t :=
   let t := eval hnf in t in
   match t with
-    true => constr:true
-  | false => constr:false
-  | _ => constr:NotConstant
+    true => constr:(true)
+  | false => constr:(false)
+  | _ => constr:(NotConstant)
   end.
 
 Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 914843727..23784cf33 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -17,14 +17,14 @@ Set Implicit Arguments.
 Ltac Zcst t :=
   match isZcst t with
     true => t
-  | _ => constr:NotConstant
+  | _ => constr:(NotConstant)
   end.
 
 Ltac isZpow_coef t :=
   match t with
   | Zpos ?p => isPcst p
-  | Z0 => constr:true
-  | _ => constr:false
+  | Z0 => constr:(true)
+  | _ => constr:(false)
   end.
 
 Notation N_of_Z := Z.to_N (only parsing).
@@ -32,7 +32,7 @@ Notation N_of_Z := Z.to_N (only parsing).
 Ltac Zpow_tac t :=
  match isZpow_coef t with
  | true => constr:(N_of_Z t)
- | _ => constr:NotConstant
+ | _ => constr:(NotConstant)
  end.
 
 Ltac Zpower_neg :=
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index aad0bb44d..8dadc2419 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 070d1e9c7..a327bbf2a 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 52dae265b..04fa59075 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 7069bba43..8462d3627 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 6c4d4ae98..ce9099059 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.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index c41eb2fa2..627a1a495 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -452,7 +452,7 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     end
   in
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8d942d908..81b31d783 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -465,7 +465,7 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     end
   in
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 145d451f0..190397ae4 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "by" tactic3(t) :=
-  setoidreplace (default_relation x y) ltac:t.
+  setoidreplace (default_relation x y) ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceat (default_relation x y) ltac:t o.
+  setoidreplaceat (default_relation x y) ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id)
   "by" tactic3(t) :=
-  setoidreplacein (default_relation x y) id ltac:t.
+  setoidreplacein (default_relation x y) id ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceinat (default_relation x y) id ltac:t o.
+  setoidreplaceinat (default_relation x y) id ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel) :=
@@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "by" tactic3(t) :=
-  setoidreplace (rel x y) ltac:t.
+  setoidreplace (rel x y) ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceat (rel x y) ltac:t o.
+  setoidreplaceat (rel x y) ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
@@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "by" tactic3(t) :=
-  setoidreplacein (rel x y) id ltac:t.
+  setoidreplacein (rel x y) id ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceinat (rel x y) id ltac:t o.
+  setoidreplaceinat (rel x y) id ltac:(t) o.
 
 (** The [add_morphism_tactic] tactic is run at each [Add Morphism]
    command before giving the hand back to the user to discharge the
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index 215b8bd58..d160f5f1d 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -19,13 +19,13 @@ Local Open Scope list_scope.
 
 Ltac isInt31cst_lst l :=
  match l with
- | nil => constr:true
+ | nil => constr:(true)
  | ?t::?l => match t with
                | D1 => isInt31cst_lst l
                | D0 => isInt31cst_lst l
-               | _ => constr:false
+               | _ => constr:(false)
              end
- | _ => constr:false
+ | _ => constr:(false)
  end.
 
 Ltac isInt31cst t :=
@@ -38,17 +38,17 @@ Ltac isInt31cst t :=
       ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
       ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
     in isInt31cst_lst l
- | Int31.On => constr:true
- | Int31.In => constr:true
- | Int31.Tn => constr:true
- | Int31.Twon => constr:true
- | _ => constr:false
+ | Int31.On => constr:(true)
+ | Int31.In => constr:(true)
+ | Int31.Tn => constr:(true)
+ | Int31.Twon => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac Int31cst t :=
  match isInt31cst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** The generic ring structure inferred from the Cyclic structure *)
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index ec495d094..56cb9bbc2 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -148,26 +148,26 @@ Ltac isBigZcst t :=
  match t with
  | BigZ.Pos ?t => isBigNcst t
  | BigZ.Neg ?t => isBigNcst t
- | BigZ.zero => constr:true
- | BigZ.one => constr:true
- | BigZ.two => constr:true
- | BigZ.minus_one => constr:true
- | _ => constr:false
+ | BigZ.zero => constr:(true)
+ | BigZ.one => constr:(true)
+ | BigZ.two => constr:(true)
+ | BigZ.minus_one => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigZcst t :=
  match isBigZcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Ltac BigZ_to_N t :=
  match t with
  | BigZ.Pos ?t => BigN_to_N t
- | BigZ.zero => constr:0%N
- | BigZ.one => constr:1%N
- | BigZ.two => constr:2%N
- | _ => constr:NotConstant
+ | BigZ.zero => constr:(0%N)
+ | BigZ.one => constr:(1%N)
+ | BigZ.two => constr:(2%N)
+ | _ => constr:(NotConstant)
  end.
 
 (** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 29a1145e0..ec1017f50 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -119,10 +119,10 @@ Qed.
 
 Ltac isStaticWordCst t :=
  match t with
- | W0 => constr:true
+ | W0 => constr:(true)
  | WW ?t1 ?t2 =>
    match isStaticWordCst t1 with
-   | false => constr:false
+   | false => constr:(false)
    | true => isStaticWordCst t2
    end
  | _ => isInt31cst t
@@ -139,30 +139,30 @@ Ltac isBigNcst t :=
  | BigN.N6 ?t => isStaticWordCst t
  | BigN.Nn ?n ?t => match isnatcst n with
    | true => isStaticWordCst t
-   | false => constr:false
+   | false => constr:(false)
    end
- | BigN.zero => constr:true
- | BigN.one => constr:true
- | BigN.two => constr:true
- | _ => constr:false
+ | BigN.zero => constr:(true)
+ | BigN.one => constr:(true)
+ | BigN.two => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigNcst t :=
  match isBigNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Ltac BigN_to_N t :=
  match isBigNcst t with
  | true => eval vm_compute in (BigN.to_N t)
- | false => constr:NotConstant
+ | false => constr:(NotConstant)
  end.
 
 Ltac Ncst t :=
  match isNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fe38ea4f2..850afe534 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -104,18 +104,18 @@ Ltac isBigQcst t :=
  | BigQ.Qz ?t => isBigZcst t
  | BigQ.Qq ?n ?d => match isBigZcst n with
              | true => isBigNcst d
-             | false => constr:false
+             | false => constr:(false)
              end
- | BigQ.zero => constr:true
- | BigQ.one => constr:true
- | BigQ.minus_one => constr:true
- | _ => constr:false
+ | BigQ.zero => constr:(true)
+ | BigQ.one => constr:(true)
+ | BigQ.minus_one => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigQcst t :=
  match isBigQcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Add Field BigQfield : BigQfieldth
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 27e1ca844..17f05c511 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -238,8 +238,8 @@ Ltac inject_left H :=
 Ltac inject_right H :=
   progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H.
 
-Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
-Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
+Ltac autoinjections_left := repeat autoinjection ltac:(inject_left).
+Ltac autoinjections_right := repeat autoinjection ltac:(inject_right).
 
 Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
   simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 66ca3e577..7384790da 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -252,7 +252,7 @@ Ltac autoinjection tac :=
 
 Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H.
 
-Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject).
+Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)).
 
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)
 
diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
index 2465f0399..e57af7311 100644
--- a/theories/Reals/Ranalysis_reg.v
+++ b/theories/Reals/Ranalysis_reg.v
@@ -35,7 +35,7 @@ Qed.
 
 (**********)
 Ltac intro_hyp_glob trm :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       match goal with
         |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
@@ -55,7 +55,7 @@ Ltac intro_hyp_glob trm :=
         | _ => idtac
       end
     | (?X1 / ?X2)%F =>
-      let aux := constr:X2 in
+      let aux := constr:(X2) in
         match goal with
           | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
             intro_hyp_glob X1; intro_hyp_glob X2
@@ -82,7 +82,7 @@ Ltac intro_hyp_glob trm :=
         | _ => idtac
       end
     | (/ ?X1)%F =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
           | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
             intro_hyp_glob X1
@@ -108,7 +108,7 @@ Ltac intro_hyp_glob trm :=
     | (pow_fct _) => idtac
     | Rabs => idtac
     | ?X1 =>
-      let p := constr:X1 in
+      let p := constr:(X1) in
         match goal with
           | _:(derivable p) |- _ => idtac
           |  |- (derivable p) => idtac
@@ -130,7 +130,7 @@ Ltac intro_hyp_glob trm :=
 
 (**********)
 Ltac intro_hyp_pt trm pt :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       match goal with
         |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
@@ -156,7 +156,7 @@ Ltac intro_hyp_pt trm pt :=
         | _ => idtac
       end
     | (?X1 / ?X2)%F =>
-      let aux := constr:X2 in
+      let aux := constr:(X2) in
         match goal with
           | _:(aux pt <> 0) |- (derivable_pt _ _) =>
             intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
@@ -202,7 +202,7 @@ Ltac intro_hyp_pt trm pt :=
         | _ => idtac
       end
     | (/ ?X1)%F =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
           | _:(aux pt <> 0) |- (derivable_pt _ _) =>
             intro_hyp_pt X1 pt
@@ -249,7 +249,7 @@ Ltac intro_hyp_pt trm pt :=
         | _ => idtac
       end
     | ?X1 =>
-      let p := constr:X1 in
+      let p := constr:(X1) in
         match goal with
           | _:(derivable_pt p pt) |- _ => idtac
           |  |- (derivable_pt p pt) => idtac
@@ -578,89 +578,89 @@ Ltac is_cont_glob :=
 
 (**********)
 Ltac rew_term trm :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 + X4))
-              | _ => constr:(p1 + p2)%F
+              | _ => constr:((p1 + p2)%F)
             end
-          | _ => constr:(p1 + p2)%F
+          | _ => constr:((p1 + p2)%F)
         end
     | (?X1 - ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 - X4))
-              | _ => constr:(p1 - p2)%F
+              | _ => constr:((p1 - p2)%F)
             end
-          | _ => constr:(p1 - p2)%F
+          | _ => constr:((p1 - p2)%F)
         end
     | (?X1 / ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
-              | _ => constr:(p1 / p2)%F
+              | _ => constr:((p1 / p2)%F)
             end
           | _ =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
-              | _ => constr:(p1 / p2)%F
+            match constr:(p2) with
+              | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F)
+              | _ => constr:((p1 / p2)%F)
             end
         end
     | (?X1 * / ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
-              | _ => constr:(p1 / p2)%F
+              | _ => constr:((p1 / p2)%F)
             end
           | _ =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
-              | _ => constr:(p1 / p2)%F
+            match constr:(p2) with
+              | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F)
+              | _ => constr:((p1 / p2)%F)
             end
         end
     | (?X1 * ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 * X4))
-              | _ => constr:(p1 * p2)%F
+              | _ => constr:((p1 * p2)%F)
             end
-          | _ => constr:(p1 * p2)%F
+          | _ => constr:((p1 * p2)%F)
         end
     | (- ?X1) =>
       let p := rew_term X1 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X2) => constr:(fct_cte (- X2))
-          | _ => constr:(- p)%F
+          | _ => constr:((- p)%F)
         end
     | (/ ?X1) =>
       let p := rew_term X1 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X2) => constr:(fct_cte (/ X2))
-          | _ => constr:(/ p)%F
+          | _ => constr:((/ p)%F)
         end
-    | (?X1 AppVar) => constr:X1
+    | (?X1 AppVar) => constr:(X1)
     | (?X1 ?X2) =>
       let p := rew_term X2 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X3) => constr:(fct_cte (X1 X3))
           | _ => constr:(comp X1 p)
         end
-    | AppVar => constr:id
+    | AppVar => constr:(id)
     | (AppVar ^ ?X1) => constr:(pow_fct X1)
     | (?X1 ^ ?X2) =>
       let p := rew_term X1 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3))
           | _ => constr:(comp (pow_fct X2) p)
         end
@@ -669,7 +669,7 @@ Ltac rew_term trm :=
 
 (**********)
 Ltac deriv_proof trm pt :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
         constr:(derivable_pt_plus X1 X2 pt p1 p2)
@@ -684,14 +684,14 @@ Ltac deriv_proof trm pt :=
         | id:(?X2 pt <> 0) |- _ =>
           let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
             constr:(derivable_pt_div X1 X2 pt p1 p2 id)
-        | _ => constr:False
+        | _ => constr:(False)
       end
     | (/ ?X1)%F =>
       match goal with
         | id:(?X1 pt <> 0) |- _ =>
           let p1 := deriv_proof X1 pt in
             constr:(derivable_pt_inv X1 pt p1 id)
-        | _ => constr:False
+        | _ => constr:(False)
       end
     | (comp ?X1 ?X2) =>
       let pt_f1 := eval cbv beta in (X2 pt) in
@@ -710,21 +710,21 @@ Ltac deriv_proof trm pt :=
     | sqrt =>
       match goal with
         | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id)
-        | _ => constr:False
+        | _ => constr:(False)
       end
     | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt)
     | ?X1 =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
-          | id:(derivable_pt aux pt) |- _ => constr:id
+          | id:(derivable_pt aux pt) |- _ => constr:(id)
           | id:(derivable aux) |- _ => constr:(id pt)
-          | _ => constr:False
+          | _ => constr:(False)
         end
   end.
 
 (**********)
 Ltac simplify_derive trm pt :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       try rewrite derive_pt_plus; simplify_derive X1 pt;
         simplify_derive X2 pt
@@ -753,7 +753,7 @@ Ltac simplify_derive trm pt :=
     | Rsqr => try rewrite derive_pt_Rsqr
     | sqrt => try rewrite derive_pt_sqrt
     | ?X1 =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
           | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ =>
             try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2);
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index d210792f9..32e13d389 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -225,11 +225,11 @@ Module MoreInt (Import I:Int).
   (** [int] to [ExprI] *)
 
   Ltac i2ei trm :=
-    match constr:trm with
-      | 0 => constr:EI0
-      | 1 => constr:EI1
-      | 2 => constr:EI2
-      | 3 => constr:EI3
+    match constr:(trm) with
+      | 0 => constr:(EI0)
+      | 1 => constr:(EI1)
+      | 2 => constr:(EI2)
+      | 3 => constr:(EI3)
       | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey)
       | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey)
       | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey)
@@ -241,7 +241,7 @@ Module MoreInt (Import I:Int).
   (** [Z] to [ExprZ] *)
 
     with z2ez trm :=
-    match constr:trm with
+    match constr:(trm) with
       | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey)
       | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey)
       | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey)
@@ -254,7 +254,7 @@ Module MoreInt (Import I:Int).
   (** [Prop] to [ExprP] *)
 
   Ltac p2ep trm :=
-    match constr:trm with
+    match constr:(trm) with
       | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey)
       | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey)
       | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey)
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index b80eb4451..f4baba190 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -30,12 +30,12 @@ Local Open Scope Z_scope.
 Ltac compute_POS :=
   match goal with
     |  |- context [(Zpos (xI ?X1))] =>
-      match constr:X1 with
+      match constr:(X1) with
 	| context [1%positive] => fail 1
 	| _ => rewrite (Pos2Z.inj_xI X1)
       end
     |  |- context [(Zpos (xO ?X1))] =>
-      match constr:X1 with
+      match constr:(X1) with
 	| context [1%positive] => fail 1
 	| _ => rewrite (Pos2Z.inj_xO X1)
       end