Changeset 2494


Ignore:
Timestamp:
Nov 26, 2012, 6:24:20 PM (7 years ago)
Author:
mckinna
Message:

Removed BJC's axiomatisation of rtlabs_to_rtl, now that RTL/RTLabsToRTL.ma rechecks.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2492 r2494  
    1616  return 〈init_cost,p',p〉.
    1717
    18 (* Recent changes have temporarily stopped the back-end from checking, so
    19    axiomatise it for a little while.
    20 include "RTLabs/RTLabsToRTL.ma". *) include "RTL/RTL.ma". axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
     18include "RTLabs/RTLabsToRTL.ma".
    2119include "RTL/RTLToERTL.ma".
    2220include "ERTL/ERTLToLTL.ma".
Note: See TracChangeset for help on using the changeset viewer.