Changeset 1153 for Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma
- Timestamp:
- Aug 30, 2011, 6:55:12 PM (9 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1110-1132,1136-1150
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma
r1105 r1153 718 718 qed. 719 719 720 definition cminor_ to_rtlabs : Cminor_program → res RTLabs_program ≝720 definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝ 721 721 transform_partial_program ??? 722 722 (transf_partial_fundef ?? c2ra_function). … … 724 724 include "Cminor/initialisation.ma". 725 725 726 definition cminor_ init_to_rtlabs : Cminor_program → res RTLabs_program ≝727 λp. let p' ≝ replace_init p in cminor_ to_rtlabs p.726 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ 727 λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracChangeset
for help on using the changeset viewer.