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

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