Commit f48fd393 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Fix merge errors in FPRangeValidator

parent 59976fa6
......@@ -129,8 +129,9 @@ Proof.
prove_fprangeval (join m0 m1) v L1 R.
- Daisy_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval (join3 m0 m1 m2) v L1 R.
- Daisy_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
Qed.
......
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