Changeset 2492 for src/compiler.ma
- Timestamp:
- Nov 26, 2012, 11:52:51 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/compiler.ma
r2475 r2492 18 18 (* Recent changes have temporarily stopped the back-end from checking, so 19 19 axiomatise it for a little while. 20 include "RTLabs/RTLabsToRTL.ma". 20 include "RTLabs/RTLabsToRTL.ma". *) include "RTL/RTL.ma". axiom rtlabs_to_rtl: RTLabs_program → rtl_program. 21 21 include "RTL/RTLToERTL.ma". 22 22 include "ERTL/ERTLToLTL.ma". … … 35 35 let p ≝ ltl_to_lin p in 36 36 lin_to_asm p. 37 *)38 include "ASM/ASM.ma".39 axiom back_end : RTLabs_program → pseudo_assembly_program.40 37 41 38 include "ASM/Assembly.ma".
Note: See TracChangeset
for help on using the changeset viewer.