X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=25e2523bfefff413a6b4680d4d08336789adc0d7;hp=7624c3153c444d1414b1223eb1429d2f7a36c5dd;hb=6b017fc7346850c589273befe5faef9ee57bd53d;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 7624c31..25e2523 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -26,9 +26,9 @@ Section ToLatex.
 
   Fixpoint kind2latex (k:Kind) : string :=
     match k with
-    | KindType                     => "\star"
-    | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
-    | KindTypeFunction k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
+    | ★                            => "\star"
+    | ★  ⇛ k2                      => "\star\Rightarrow "+++kind2latex k2
+    | k1 ⇛ k2                      => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
     | KindUnliftedType             => "\text{\tt{\#}}"
     | KindUnboxedTuple             => "\text{\tt{(\#)}}"
     | KindArgType                  => "\text{\tt{??}}"