diff options
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index cb9f4fc5..d997015f 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -220,8 +220,8 @@ Proof. apply eval_negf; auto. apply eval_absf; auto. apply eval_singleoffloat; auto. - apply eval_intoffloat; auto. - apply eval_intuoffloat; auto. + remember (Float.intoffloat f) as oi; destruct oi; inv H0. eapply eval_intoffloat; eauto. + remember (Float.intuoffloat f) as oi; destruct oi; inv H0. eapply eval_intuoffloat; eauto. apply eval_floatofint; auto. apply eval_floatofintu; auto. Qed. |