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

Timestamp:

Oct 6, 2011, 6:45:54 PM (9 years ago)

Author:

campbell

Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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

@@ -155 +155 @@
    responsible for initialisation and we only give the size of each variable. *)
 
-definition Cminor_program ≝ program (fundef internal_function) (list init_data).
+definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
 
-definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
+definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.