Library mcertikos.proc.QThreadGenLinkSource
Require Import LinkSourceTemplate.
Require Import PThread.
Definition PQThread_module: link_module :=
{|
lm_cfun :=
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition PQThread_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
link_impl PQThread_module pthread.
Require Import PThread.
Definition PQThread_module: link_module :=
{|
lm_cfun :=
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition PQThread_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
link_impl PQThread_module pthread.