rm commented-out stuff

1 files changed, 0 insertions, 86 deletions

diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v
index 642bc59d..fc04c77e 100644
--- a/backend/Profilingproof.v
+++ b/backend/Profilingproof.v
@@ -655,92 +655,6 @@ Proof.
     + constructor; auto.
 Qed.
 
-(*
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Inop; eauto with firstnop.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iop with (v:=v); eauto with firstnop.
-      rewrite <- H0.
-      apply eval_operation_preserved.
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
-      all: rewrite <- H0.
-      all: auto using eval_addressing_preserved, symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Istore; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Icall.
-      apply match_pc_same. exact H.
-      apply find_function_translated.
-      exact H0.
-      apply sig_preserved.
-    + constructor.
-      constructor; auto.
-      constructor.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Itailcall.
-      apply match_pc_same. exact H.
-      apply find_function_translated.
-      exact H0.
-      apply sig_preserved.
-      unfold transf_function; simpl.
-      eassumption.
-    + constructor; auto.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Ibuiltin; eauto with firstnop.
-      eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-    + constructor; auto.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Icond; eauto with firstnop.
-    + constructor; auto.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Ijumptable; eauto with firstnop.
-    + constructor; auto.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Ireturn; eauto with firstnop.
-    + constructor; auto.
-  - left. econstructor. split.
-    + eapply plus_two.
-      * eapply exec_function_internal; eauto with firstnop.
-      * eapply exec_Inop.
-        unfold transf_function; simpl.
-        rewrite PTree.gss.
-        reflexivity.
-      * auto.
-    + constructor; auto.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_function_external; eauto with firstnop.
-      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-    + constructor; auto.
-  - left.
-    inv STACKS. inv H1.
-    econstructor; split.
-    + eapply plus_one. eapply exec_return; eauto.
-    + constructor; auto.
-Qed.
- *)
-
 Lemma transf_initial_states:
   forall S1, RTL.initial_state prog S1 ->
   exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.