diff options
Diffstat (limited to 'plugins/setoid_ring/Ring.v')
| -rw-r--r-- | plugins/setoid_ring/Ring.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index a0844100..77576cb9 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]). |