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.
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.