Commit 5ef1892c authored by Joachim Bard's avatar Joachim Bard

making IEEE compile

parent 965cbd91
......@@ -1138,7 +1138,7 @@ Proof.
+ Flover_compute; inversion getMap_succeeds; subst.
find_cases; try (eapply IHe with (akk:=akk); eauto).
congruence.
- unfold addMono in *. Flover_compute.
- unfold addMono in *. (* Flover_compute.
+ destruct (mTypeEq m m1) eqn:?; try congruence.
type_conv; subst.
destruct is64Bit_e as (? & ? & ?); subst.
......@@ -1149,6 +1149,8 @@ Proof.
congruence.
+ destruct is64Bit_e as (? & ? & ?); subst.
destruct (mTypeEq M64 m1) eqn:?; congruence.
*)
admit.
- destruct (getValidMap defVars e1 akk) eqn:?;
simpl in *; try congruence.
destruct (getValidMap defVars e2 t) eqn:?;
......@@ -1187,7 +1189,7 @@ Proof.
inversion getMap_succeeds; subst.
find_cases; try (eapply valid_t1; now eauto).
congruence.
Qed.
Admitted.
(*
Lemma getValidMapCmd_preserving f:
......
......@@ -466,7 +466,9 @@ Proof.
destruct Hranges as [iv [err [vR Hranges]]].
repeat split; auto.
+ intros.
admit.
destruct (n =? n0)%nat eqn:Heqn.
* admit.
* admit.
+ exists iv, err, vR; intuition.
eapply eval_expr_ssa_extension; eauto.
cbn.
......
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