X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;fp=src%2FHaskWeakToCore.v;h=290d6341344c8f80f03d266b2a1fe30e7cc70643;hp=51e61dd83aadac32525973479c7ad91b385362d9;hb=94d7c55025f5df750ce213172c5d2441b5a210e1;hpb=93b1553e602360ffcae3f2670ec3ac189a5e5df9

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 51e61dd..290d634 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -31,9 +31,6 @@ Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
-Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
-
 Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
   match wa with
   | WeakDataAlt cdc => DataAlt cdc