Ignore:
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:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

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

    r1105 r1153  
    718718qed.
    719719
    720 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     720definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    721721transform_partial_program ???
    722722  (transf_partial_fundef ?? c2ra_function).
     
    724724include "Cminor/initialisation.ma".
    725725
    726 definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
    727 λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
     726definition 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.