parenthesize Ltac [constr:] arguments

2 files changed, 6 insertions, 6 deletions

diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index a33d108fb..8ae651826 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -849,21 +849,21 @@ Implicit Arguments weqb_sound [].
 
 Ltac isWcst w :=
   match eval hnf in w with
-    | WO => constr:true
+    | WO => constr:(true)
     | WS ?b ?w' =>
       match eval hnf in b with
         | true => isWcst w'
         | false => isWcst w'
-        | _ => constr:false
+        | _ => constr:(false)
       end
-    | _ => constr:false
+    | _ => constr:(false)
   end.
 
 Ltac wcst w :=
   let b := isWcst w in
     match b with
       | true => w
-      | _ => constr:NotConstant
+      | _ => constr:(NotConstant)
     end.
 
 (* Here's how you can add a ring for a specific bit-width.
diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v
index 3eb3647a1..8fa8c4a86 100644
--- a/src/Tactics/Nsatz.v
+++ b/src/Tactics/Nsatz.v
@@ -25,7 +25,7 @@ Ltac nsatz_reify_equations eq zero :=
   lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
     (?variables, ?le) =>
     lazymatch (eval compute in (List.rev le)) with
-    | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal)
+    | ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal))
     end
   end.
 
@@ -56,7 +56,7 @@ Ltac nsatz_compute_get_leading_coefficient :=
 
 Ltac nsatz_compute_get_certificate :=
   lazymatch goal with
-    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b)
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b))
   end.
 
 Ltac nsatz_rewrite_and_revert domain :=