diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 11:16:03 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 14:52:53 +0100 |
commit | d5656a6c28f79d59590d4fde60c5158a649d1b65 (patch) | |
tree | eac22126e5577742b22d731e53e9b49e81d40095 /theories/Numbers/Integer | |
parent | 143bb68613bcb314e2feffd643f539fba9cd3912 (diff) |
Making parentheses mandatory in tactic scopes.
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 22 |
1 files changed, 11 insertions, 11 deletions
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 *) |