Library ArchSem.ArchInst

Require Import Interface.
Require Import TermModels.
Require Import CandidateExecutions.
Require Import GenPromising.
Require Import SeqModel.
Require Import ISAManip.

Module ArchInst (A : Arch) (NC : NoCHERI A).
  Module Interface := Interface A.
  Module TM := TermModels A Interface.
  Module Cand := CandidateExecutions A Interface TM NC.
  Module GenPro := GenPromising A Interface TM.
  Module SeqModel := SequentialModel A Interface TM NC.
  Module ISAManip := ISAManip A Interface TM.
End ArchInst.