aboutsummaryrefslogtreecommitdiff
path: root/Bedrock
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-06-20 14:28:02 -0400
committerGravatar Andres Erbsen <andreser@mit.edu>2016-06-20 14:28:02 -0400
commit1a5130702303e2843ab458e2566bef293c6947cd (patch)
tree043153c61175d372f7a92c495d7189e64b556ce3 /Bedrock
parent4bb42c36190c360f8d2fecc865ed9e822deddf26 (diff)
parenthesize Ltac [constr:] arguments
Diffstat (limited to 'Bedrock')
-rw-r--r--Bedrock/Word.v8
1 files changed, 4 insertions, 4 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.