Changeset 2116

Timestamp:

06/27/12 11:46:36 (11 months ago)

Author:

sacerdot

Message:

load_code_memory will be moved into Fetch.ma in the next commit.
This is a bit weird: we could split a Load.ma file from Fetch.ma.

Files:

• src/compiler.ma (modified) (1 diff)

src/compiler.ma

@@ -62 +62 @@
 
 include "common/StructuredTraces.ma".
+include "ASM/Fetch.ma". (* For load_code_memory only *)
 
 definition in_clight_program : costlabel → Prop ≝ λ_.True.