Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 4 insertions, 6 deletions

diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index ca8e915..f3dd9ed 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -616,15 +616,13 @@ Qed.
 
 
 (** The preservation of the observable behavior of the program then
-  follows, using the generic preservation theorem
-  [Smallstep.simulation_opt_preservation]. *)
+  follows. *)
 
 Theorem transf_program_correct:
-  forall (beh: program_behavior), not_wrong beh ->
-  exec_program prog beh -> exec_program tprog beh.
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  unfold exec_program; intros.
-  eapply simulation_opt_preservation with (measure := measure); eauto.
+  eapply forward_simulation_opt with (measure := measure); eauto.
+  eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact transf_step_correct.