Module Qcert.Common.TypingRuntime


Require Export ForeignData.
Require Export CommonSystem.

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