Module Qcert.Data.Model.Constants


Require Import String.
Require Import List.
Require Import Data.
Require Import ForeignData.

Section Constants.
  
  Context {fdata:foreign_data}.

  Definition WORLD:string := "WORLD"%string.
    
  Definition mkWorld (world:list data) : list (string*data)
    := (WORLD,(dcoll world))::nil.

  Definition pd_bindings := list (string*option data).
End Constants.