From: Adam Megacz Date: Fri, 25 Mar 2011 18:09:10 +0000 (-0700) Subject: move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=94d7c55025f5df750ce213172c5d2441b5a210e1 move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons --- diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 055d588..36399a0 100644 --- 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 --- 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 --- 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