diff options
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 9c851573..de2fd422 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -273,8 +273,8 @@ Proof. destruct a1; destruct a0; eauto; constructor. (* selectl *) - inv H2; simpl; try constructor. - + destruct (Int64.eq _ _); apply binop_long_sound; trivial. - + destruct (Int64.eq _ _); + + destruct (Int.eq _ _); apply binop_long_sound; trivial. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. |