Commit cb3b7782 authored by Heiko Becker's avatar Heiko Becker

Fix compilation error in IEEE_connection.v

parent 96bc2e7e
......@@ -1055,8 +1055,7 @@ Proof.
+ destruct bstep_sound as [eval_sound bstep_sound].
rewrite eval_float_e in bstep_sound; unfold optionBind in bstep_sound.
auto.
+ unfold RealRangeArith.vars_typed.
intros. unfold updEnv. destruct (v1 =? n) eqn:?.
+ intros. unfold updEnv. destruct (v1 =? n) eqn:?.
* eexists; exists M64; repeat split; eauto.
{ rewrite Nat.eqb_eq in Heqb; subst; auto. }
{ eapply FPRangeValidator_sound; eauto.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment