X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=1471e51ef99216243ce2f9994e83e0c428833370;hb=32436fdf380f7f2efc7a70896268509e7b3e0d6f;hp=25e2523bfefff413a6b4680d4d08336789adc0d7;hpb=6b017fc7346850c589273befe5faef9ee57bd53d;p=coq-hetmet.git

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 25e2523..1471e51 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -171,9 +171,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 +184,7 @@ Section ToLatex.
       | RApp          _ _ _ _ _ _ _     => "App"
       | RLet          _ _ _ _ _ _ _     => "Let"
       | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
-      | RLetRec       _ _ _ _ _         => "LetRec"
+      | RLetRec       _ _ _ _ _ _       => "LetRec"
       | RCase         _ _ _ _ _ _ _ _   => "Case"
       | RBrak         _ _ _ _ _ _       => "Brak"
       | REsc          _ _ _ _ _ _       => "Esc"