Changeset 1139 for src/Clight/Csyntax.ma

Timestamp:

Aug 30, 2011, 12:47:18 PM (10 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:

• src/Clight/Csyntax.ma (modified) (1 diff)

src/Clight/Csyntax.ma

@@ -318 +318 @@
   data.  See module [AST] for more details. *)
 
-definition clight_program : Type[0] ≝ program clight_fundef type.
+definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
 
 (* * * Operations over types *)