Changeset 2492 for src/compiler.ma

Timestamp:

Nov 26, 2012, 11:52:51 AM (8 years ago)

Author:

campbell

Message:

Reduce axiomatisation in compiler.ma.

File:

• src/compiler.ma (modified) (2 diffs)

src/compiler.ma

@@ -18 +18 @@
 (* Recent changes have temporarily stopped the back-end from checking, so
    axiomatise it for a little while.
-include "RTLabs/RTLabsToRTL.ma".
+include "RTLabs/RTLabsToRTL.ma". *) include "RTL/RTL.ma". axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
 include "RTL/RTLToERTL.ma".
 include "ERTL/ERTLToLTL.ma".
@@ -35 +35 @@
   let p ≝ ltl_to_lin p in
           lin_to_asm p.
-*)
-include "ASM/ASM.ma".
-axiom back_end : RTLabs_program → pseudo_assembly_program.
 
 include "ASM/Assembly.ma".