Library liblayers.compcertx.ClightModules

Require Export liblayers.logic.Modules.
Require Export liblayers.logic.PTreeModules.
Require Export compcert.common.AST.
Require Export compcert.cfrontend.Clight.
Require Export compcert.cfrontend.Ctypes.

Definition cmodule := ptree_module Clight.function (globvar Ctypes.type).

Global Instance cmodule_ops : ModuleOps ident function (globvar type) cmodule :=
  ptree_module_ops.

Global Instance cmodule_prf : Modules ident function (globvar type) cmodule :=
  ptree_module_prf.