move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 055d588..36399a0 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -15,9 +15,6 @@ Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 
-Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
-
 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
 Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 24fc00f..0592f3a 100644 (file)
--- 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".

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 51e61dd..290d634 100644 (file)
--- 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