Commit 48c2792e authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix bug in Coq files

parent de0c5b3a
......@@ -141,7 +141,6 @@ Section ComputableErrors.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
inversion eval_float; subst.
unfold envApproximatesPrecond in absenv_approx_p.
unfold precondValidForExec in cenv_approx_p.
specialize (absenv_approx_p v).
specialize (cenv_approx_p v).
......@@ -16,8 +16,7 @@ Fixpoint approximatesPrecond (e:exp Q) (absenv:analysisResult) (P:precond) :=
|Const n => true
|Var v => true
|Param v =>
let iv_pre := P v in
let (vprelo, vprehi) := iv_pre in
let (vprelo, vprehi) := P v in
let (iv,err) := absenv (Param Q v) in
let (vlo,vhi) := iv in
andb (Qleb vlo vprelo) (Qleb vprehi vhi)
......@@ -29,7 +28,7 @@ Theorem approximatesPrecond_sound e absenv P:
forall v, In v (freeVars Q e) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
induction e; unfold envApproximatesPrecond.
induction e; unfold approximatesPrecond.
- intros approx_true v v_in_fV; simpl in *; contradiction.
- intros approx_true v v_in_fV; simpl in *.
unfold isSupersetIntv.
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