X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=41e857c3086dfa234c3b534d9b6315915635da4a;hb=bb960df7c29c851ca9d13f2d0c8f351ac24045ca;hp=f31560388e24d455155b185890a0b47455b3c3b8;hpb=8c26722a1ee110077968a8a166eb7130266b2035;p=coq-hetmet.git

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index f315603..41e857c 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -12,23 +12,20 @@ Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskCoreTypes.
 
-(* escapifies any characters which might cause trouble for LaTeX *)
-Variable sanitizeForLatex    : string      -> string.        Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
-
 Open Scope string_scope.
 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{??}}"
@@ -171,9 +168,10 @@ Section ToLatex.
   Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
     match r with
       | RURule        _ _ _ _ r         => nd_urule2latex r
-      | RNote         _ _ _             => "Note"
+      | RNote         _ _ _ _ _ _       => "Note"
       | RLit          _ _ _ _           => "Lit"
       | RVar          _ _ _ _           => "Var"
+      | RGlobal       _ _ _ _ _         => "Global"
       | RLam          _ _ _ _ _ _       => "Abs"
       | RCast         _ _ _ _ _ _ _     => "Cast"
       | RAbsT         _ _ _ _ _ _       => "AbsT"
@@ -183,7 +181,7 @@ Section ToLatex.
       | RApp          _ _ _ _ _ _ _     => "App"
       | RLet          _ _ _ _ _ _ _     => "Let"
       | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
-      | RLetRec       _ _ _ _ _         => "LetRec"
+      | RLetRec       _ _ _ _ _ _       => "LetRec"
       | RCase         _ _ _ _ _ _ _ _   => "Case"
       | RBrak         _ _ _ _ _ _       => "Brak"
       | REsc          _ _ _ _ _ _       => "Esc"