X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;fp=src%2FHaskProofToLatex.v;h=edac1aa0138b67de28e95664560c46b9c5f29588;hp=4773effcb4e04424caeef1ac2d8ed7b188694634;hb=e4fcbccb71fc54544e9acc62e95d1d15ec86294b;hpb=75a0b52b9937ab6b68ed98cc24281bc9153e96b9

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 4773eff..edac1aa 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -101,7 +101,7 @@ Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath
                                       ; let body := t1'+++(rawLatexMath " ")+++t2'
                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
                 end
-  | TyFunApp   tfc lt  => bind rest = typeListToRawLatexMath false lt
+  | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
                         ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
                                  (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
                                  (rawLatexMath "}")+++