diff options
Diffstat (limited to 'ia32/Asmgenproof.v')
| -rw-r--r-- | ia32/Asmgenproof.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 5b98d277..e8c6757f 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -455,6 +455,8 @@ Remark transl_op_label: Proof. unfold transl_op; intros. destruct op; ArgsInv; auto. eapply mk_mov_label; eauto. + destruct (Int.eq_dec i Int.zero); auto. + destruct (Float.eq_dec f Float.zero); auto. eapply mk_intconv_label; eauto. eapply mk_intconv_label; eauto. eapply mk_intconv_label; eauto. |