Library mcertikos.devdrivers.AbsConsoleBuffIntroGenLinkSource
Require Import LinkSourceTemplate.
Require Import DConsoleBuffIntro.
Definition DAbsConsoleBuffIntro_module: link_module :=
{|
lm_cfun :=
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition DAbsConsoleBuffIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
link_impl DAbsConsoleBuffIntro_module dconsolebuffintro.
Require Import DConsoleBuffIntro.
Definition DAbsConsoleBuffIntro_module: link_module :=
{|
lm_cfun :=
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition DAbsConsoleBuffIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
link_impl DAbsConsoleBuffIntro_module dconsolebuffintro.