diff options
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 0722f904..8eb36d6c 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -466,7 +466,8 @@ Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. -Proof. +Admitted. +(* induction 1; intros S1' MS; inv MS. all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))) in *. all: try set (invs := (fst (preanalysis tenv f))) in *. @@ -1174,7 +1175,7 @@ Proof. apply wt_regset_assign; trivial. rewrite WTRES0. exact WTRES. -Qed. +Qed. *) Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> |