split HaskLiteralsAndTyCons into two files

[coq-hetmet.git] / src / HaskCoreToWeak.v

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 6e1b58f..ac2da8c 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -53,7 +54,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                     | WExprVar _  => Error "encountered expression variable in a modal box type"
                                     | WCoerVar _  => Error "encountered coercion variable in a modal box type"
                                   end
-                                | _                           => Error ("mis-applied modal box tycon: " +++ ct)
+                                | _                           => Error ("mis-applied modal box tycon: " +++ toString ct)
                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon
@@ -134,8 +135,8 @@ Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak
   match wt with
     | WTyCon tc        => OK (tc,acc)
     | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
-    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
-    | _                => Error ("expectTyConApp encountered " +++ wt)
+    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+    | _                => Error ("expectTyConApp encountered " +++ toString wt)
   end.
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=