Library mcertikos.ticketlog.QTicketLockOpGenLinkSource

Require Import LinkSourceTemplate.
Require Import MTicketLockOp.

Definition MQTicketLockOp_module: link_module :=
  {|
    lm_cfun :=
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MQTicketLockOp_impl `{CompCertiKOS} `{RealParams} `{WaitTime} `{MultiOracleOps0} `{MultiOracleOps} `{BigOracleOps} :=
  link_impl MQTicketLockOp_module mticketlockop.