diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-03 21:22:13 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-03 21:22:13 +0200 |
| commit | e8676a19cf20cf65eb3c57b6621919d3d7ffc065 (patch) | |
| tree | 78e2bfeedc62d873264a04aab580da45538fb522 /mppa_k1c | |
| parent | 11fbb6994667de03623640842d08f1b5ee02aac1 (diff) | |
| download | compcert-kvx-e8676a19cf20cf65eb3c57b6621919d3d7ffc065.tar.gz compcert-kvx-e8676a19cf20cf65eb3c57b6621919d3d7ffc065.zip | |
forgot this function
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 5e9eb455..7d84447e 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -472,7 +472,6 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. Qed. -(* not needed Theorem eval_static_addressing_sound_none: forall addr vargs aargs, eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = None -> @@ -490,7 +489,6 @@ Proof. inv H3; destruct addr; trivial; discriminate. Qed. - *) Theorem eval_static_operation_sound: forall op vargs m vres aargs, |