X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;fp=src%2FExtraction-prefix.hs;h=3dec80feda126a9b9ff5217689b037de9d275477;hp=b144116e884a58a096e1ab3412690278853d171f;hb=f7a6e08c97cae1c1b278c18a1904eadec4e5f010;hpb=601b57023dd6fe4295c5af8bb3f5c508618a5f64

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index b144116..3dec80f 100644
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,11 +1,14 @@
 {-# OPTIONS_GHC -fno-warn-unused-binds  #-}
 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 where
+import qualified Unique
+import qualified UniqSupply
 import qualified MkCore
 import qualified TysWiredIn
 import qualified TysPrim
 import qualified Outputable
 import qualified PrelNames
+import qualified OccName
 import qualified Name
 import qualified Literal
 import qualified Type
@@ -82,6 +85,11 @@ sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
 
+kindToCoreKind :: Kind -> TypeRep.Kind
+kindToCoreKind KindStar          = TypeRep.liftedTypeKind
+kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
+kindToCoreKind _                 = Prelude.error "kindToCoreKind does not know how to handle that"
+
 coreKindToKind :: TypeRep.Kind -> Kind
 coreKindToKind k =
   case Coercion.splitKindFunTy_maybe k of