Changeset 2019 for src/compiler.ma


Ignore:
Timestamp:
Jun 6, 2012, 6:24:43 PM (8 years ago)
Author:
campbell
Message:

Split out special induction principle for Clight from soundness file.
Put cast simplification into compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2001 r2019  
    11
    22include "Clight/label.ma".
    3 (* include "Clight/SimplifyCasts.ma". *)  definition simplify_program : clight_program → clight_program ≝ λp.p.
     3include "Clight/SimplifyCasts.ma".
    44include "Clight/switchRemoval.ma".
    55include "Clight/toCminor.ma".
Note: See TracChangeset for help on using the changeset viewer.