Changeset 1153 for Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

Timestamp:

Aug 30, 2011, 6:55:12 PM (10 years ago)

Author:

campbell

Message:

Merge trunk into branch.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• Cminor/syntax.ma (modified) (1 diff)

Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

@@ -151 +151 @@
 }.
 
-definition Cminor_program ≝ program (fundef internal_function) unit.
+(* We define two closely related versions of Cminor, the first with the original
+   initialisation data for global variables, and the second where the code is
+   responsible for initialisation and we only give the size of each variable. *)
+
+definition Cminor_program ≝ program (fundef internal_function) (list init_data).
+
+definition Cminor_noinit_program ≝ program (fundef internal_function) nat.