X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreTypes.v;h=4babf3654e91181bdec260e265d0bf8210e54b31;hp=0fbaeb5b0a432cd24fa7bc4c422d526a96645639;hb=68f41d71d573b422b04ed3f4a3eb3ab41de09a79;hpb=4ad68fe2894b35c21f2feb7b176d2b0f146ff6d3

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 0fbaeb5..4babf36 100644
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -9,7 +9,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 
 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
@@ -35,7 +36,8 @@ Extract Inductive PredType =>
 
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
-Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
+Variable coreCoercionKind : Kind -> CoreType*CoreType.
+  Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
 Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".