diff options
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 73b345d3..26df4fc7 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -533,7 +533,7 @@ Proof. - TrivialExists; simpl; congruence. - TrivialExists; simpl; congruence. - TrivialExists; simpl; congruence. - - apply eval_xorimm; assumption. + - TrivialExists. Qed. Theorem eval_divs_base: |