X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=41e857c3086dfa234c3b534d9b6315915635da4a;hb=78773cd7d2fbbd3d207bdab0931b0acf8c9eb7dd;hp=56cd74788742afab83e8e38ec699527d18195558;hpb=553474663acbc6a2ee360497e9d943d3c0b3ccb5;p=coq-hetmet.git

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 56cd747..41e857c 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -18,9 +18,6 @@ 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.
 
@@ -184,7 +181,7 @@ Section ToLatex.
       | RApp          _ _ _ _ _ _ _     => "App"
       | RLet          _ _ _ _ _ _ _     => "Let"
       | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
-      | RLetRec       _ _ _ _ _         => "LetRec"
+      | RLetRec       _ _ _ _ _ _       => "LetRec"
       | RCase         _ _ _ _ _ _ _ _   => "Case"
       | RBrak         _ _ _ _ _ _       => "Brak"
       | REsc          _ _ _ _ _ _       => "Esc"