Qcert.Basic.TypingRuntime

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