X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=716a9830a6358d6f1c442004bf6e61e0e4234fc9;hp=323c1d66c4bbcae0019dcd12815fab98ae2d5bd2;hb=d97b00a6ff6e8e2244927d17bda4b9762fc3d716;hpb=6a7c6977507488245ba4b8cabcf323920c25baef;ds=sidebyside

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 323c1d6..716a983 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -189,11 +189,9 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
-    | RLet          _ _ _ _ _ _ _     => "Let"
     | RCut          _ _ _ _ _ _ _ _   => "Cut"
     | RLeft         _ _ _ _ _ _       => "Left"
     | RRight        _ _ _ _ _ _       => "Right"
-    | RWhere        _ _ _ _ _ _ _ _   => "Where"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"