Module ErgoSpec.Backend.ForeignModel

Require Export Qcert.Data.DataSystem.

Record typing_runtime
       {ftype:foreign_type}
  : Type
  := mk_typing_runtime {
         typing_runtime_brand_model : @brand_model ftype;
       }.