Changeset 1153 for Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

Timestamp:

Aug 30, 2011, 6:55:12 PM (8 years ago)

Author:

campbell

Message:

Merge trunk into branch.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• Cminor/toRTLabs.ma (modified) (2 diffs)

Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

@@ -718 +718 @@
 qed.
 
-definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
+definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
 transform_partial_program ???
   (transf_partial_fundef ?? c2ra_function).
@@ -724 +724 @@
 include "Cminor/initialisation.ma".
 
-definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
-λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
+definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
+λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.