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

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 716a983..e85bb39 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -184,7 +184,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RGlobal       _ _ _ _ _         => "Global"
     | RLam          _ _ _ _ _ _       => "Abs"
     | RCast         _ _ _ _ _ _ _     => "Cast"
-    | RAbsT         _ _ _ _ _ _       => "AbsT"
+    | RAbsT         _ _ _ _ _ _ _     => "AbsT"
     | RAppT         _ _ _ _ _ _ _     => "AppT"
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"