Changeset 1139 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (8 years ago)
Author:
campbell
Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r961 r1139  
    318318  data.  See module [AST] for more details. *)
    319319
    320 definition clight_program : Type[0] ≝ program clight_fundef type.
     320definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
    321321
    322322(* * * Operations over types *)
Note: See TracChangeset for help on using the changeset viewer.