X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=0592f3abbdc1beb8dd823f467c56ace10dbcde4a;hb=1405918ae8ff55649f864e6fd02b0c0f74fc6607;hp=24fc00f7988ee3c7d749a172bd0313ff7f1c10ee;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda;p=coq-hetmet.git

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 24fc00f..0592f3a 100644
--- a/src/HaskLiteralsAndTyCons.v
+++ b/src/HaskLiteralsAndTyCons.v
@@ -86,3 +86,6 @@ Variable tyConToString   : TyCon   -> string.     Extract Inlined Constant tyCon
 Variable tyFunToString   : TyFun   -> string.     Extract Inlined Constant tyFunToString         => "outputableToString".
 Instance TyConToString   : ToString TyCon := { toString := tyConToString }.
 Instance TyFunToString   : ToString TyFun := { toString := tyFunToString }.
+
+Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".