X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=e79927ab5ba4ecf6e69cb82d9adb867170935581;hp=1bab8f5ea992798fee03625f45cbb2d2997beadd;hb=635ee434c9edbad1bc6c9bf5ba2b91cb8c51be8e;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 1bab8f5..e79927a 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -13,6 +13,7 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
+Require Import HaskWeak.
 Require Import HaskCoreToWeak.
 
 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
@@ -563,9 +564,9 @@ Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat)
       end
     | TArrow => "(->)"
     | TAll   k f           => let alpha := "tv"+++n
-                              in "(forall "+++ alpha +++ "{:}"+++ k +++")"+++
+                              in "(forall "+++ alpha +++ ":"+++ k +++")"+++
                                    typeToString' false (S n) (f n)
-    | TCode  ec t          => "<["+++(typeToString' true n ec)+++"]>@"+++(typeToString' false n t)
+    | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
     | TyFunApp   tfc lt    => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
   end
   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=