diff options
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index d6b99ed..672f804 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1532,6 +1532,8 @@ Proof. inv H0; simpl in H; inv H. simpl. destruct (Float.longuoffloat f0); simpl in *; inv H1. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H0; simpl in H; inv H. simpl. TrivialExists. Qed. (** Compatibility of [eval_binop] with respect to [val_inject]. *) |