Commit 7a686633 authored by Joachim Bard's avatar Joachim Bard

fixing 1 admit

parent efe84342
......@@ -62,12 +62,10 @@ Proof.
intros. cbn in *; congruence. }
exists Gamma; intros approxEnv_E1E2.
destruct subdivs.
- edestruct result_checking_sound; eauto.
- edestruct result_checking_sound as (validR & validFPR & validErr); eauto.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single; eauto.
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & H4); eauto.
repeat eexists; eauto.
+ (* destruct H3 earlier *) admit.
+ (* add validFPRagnes to ResultChecker soundness *) admit.
- (* general version of subdivs_checking_sound *) admit.
Admitted.
......
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