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

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 015d02e..56cd747 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -171,7 +171,7 @@ 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"