diff options
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index bb04f786..74101f53 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -522,7 +522,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* addrsymbol *) - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)... (* addrstack *) - - destruct sp... apply Val.Vptr_has_type. + - destruct sp... (* castsigned *) - destruct v0... - destruct v0... @@ -532,8 +532,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* neg, sub *) - destruct v0... - unfold Val.sub. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... (* mul, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... @@ -582,7 +580,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... - unfold Val.subl. destruct v0; destruct v1... unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... + destruct (eq_block b b0)... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... |