Library mcertikos.ticketlog.HTicketLockOpGenLinkSource

Require Import LinkSourceTemplate.
Require Import MQTicketLockOp.

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

Section WITHORACLE.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Definition MHTicketLockOp_impl `{CompCertiKOS} `{RealParams} :=
    link_impl MHTicketLockOp_module mqticketlockop.
End WITHORACLE.