From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 14 Mar 2011 08:51:16 +0000 (-0700)
Subject: fix bugs in LaTeX output
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=62b3e1780b7c86017e720e11048fd48e1ddbaa5a

fix bugs in LaTeX output
---

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 :=