Commit a0c5b3bb authored by Heiko Becker's avatar Heiko Becker

Remove unnecessary comment

parent 1f1690ef
......@@ -14,7 +14,6 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
match e with
|Var v => false
|Param v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
(* A constant will be a point intv. Take maxAbs never the less *)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
......@@ -1137,4 +1136,4 @@ Proof.
split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. }
+ inversion valid_error.
Qed.
Qed.
\ No newline at end of file
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