diff options
Diffstat (limited to 'plugins/setoid_ring/Ring.v')
| -rw-r--r-- | plugins/setoid_ring/Ring.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index c44c2edfca..7e53c23de0 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -14,7 +14,7 @@ Require Export Ring_tac. Lemma BoolTheory : ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)). -split; simpl in |- *. +split; simpl. destruct x; reflexivity. destruct x; destruct y; reflexivity. destruct x; destruct y; destruct z; reflexivity. |