Module Syntax

Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Smallstep.
Require Import Globalenvs.
Require Import Linking.
Require Import CoqlibC.
Require Import sflib.

Require Import ModSem Mod Skeleton LinkingC.

Definition program := list Mod.t.