Library mcertikos.mm.PTInitGenLinkSource

Require Import LinkSourceTemplate.
Require Import MPTKernCSource.
Require Import MPTKern.

Definition MPTInit_module :=
  {|
    lm_cfun :=
      lcf pt_init f_pt_init ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MPTInit_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp}:=
  link_impl MPTInit_module mptkern.