diff options
Diffstat (limited to 'x86/Op.v')
| -rw-r--r-- | x86/Op.v | 14 |
1 files changed, 6 insertions, 8 deletions
@@ -400,9 +400,9 @@ Definition eval_operation | Odivfs, v1::v2::nil => Some(Val.divfs v1 v2) | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) - | Ointoffloat, v1::nil => Val.intoffloat v1 + | Ointoffloat, v1::nil => Some(Val.maketotal (Val.intoffloat v1)) | Ofloatofint, v1::nil => Val.floatofint v1 - | Ointofsingle, v1::nil => Val.intofsingle v1 + | Ointofsingle, v1::nil => Some(Val.maketotal (Val.intofsingle v1)) | Osingleofint, v1::nil => Val.singleofint v1 | Olongoffloat, v1::nil => Val.longoffloat v1 | Ofloatoflong, v1::nil => Val.floatoflong v1 @@ -730,9 +730,9 @@ Proof with (try exact I; try reflexivity). destruct v0; destruct v1... destruct v0... destruct v0... - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... + destruct v0... simpl; destruct (Float.to_int f)... destruct v0; simpl in H0; inv H0... - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2... + destruct v0... simpl; destruct (Float32.to_int f)... destruct v0; simpl in H0; inv H0... destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2... destruct v0; simpl in H0; inv H0... @@ -1298,11 +1298,9 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. - exists (Vint i); auto. + inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto. inv H4; simpl in H1; inv H1. simpl. TrivialExists. - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. - exists (Vint i); auto. + inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto. inv H4; simpl in H1; inv H1. simpl. TrivialExists. inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2. exists (Vlong i); auto. |