diff options
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5b2ad9b5..480acbb9 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1250,8 +1250,8 @@ Proof. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. - inv H0; inv H; TrivialOp. - inv H0; inv H; TrivialOp. + inv H0; inv H. destruct (Float.intoffloat f0); simpl in H1; inv H1. TrivialOp. + inv H0; inv H. destruct (Float.intuoffloat f0); simpl in H1; inv H1. TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. Qed. |