Module Qcert.Data.ForeignRuntime

Require Export ForeignData.
Require Export ForeignOperators.

Class foreign_runtime : Type
  := mk_foreign_runtime {
         foreign_runtime_data :> foreign_data
         ; foreign_runtime_operators :> foreign_operators
       }.