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

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 1bab8f5..81beb65 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -563,9 +563,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 :=