diff options
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 27a0fd01..b42503f8 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -490,6 +490,9 @@ Proof. red; intros until y; unfold xor; case (xor_match a b); intros; InvEval. rewrite Val.xor_commut. apply eval_xorimm; auto. apply eval_xorimm; auto. + subst x. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. + rewrite <- Val.not_xor. rewrite Val.xor_commut. TrivialExists. + subst y. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists. TrivialExists. Qed. |