X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=e85bb395429607e55eaf6490bb2acd2843975fe8;hp=99af119a13048dcfd7ff342a9cb41b5bb8a8bd9d;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 99af119..e85bb39 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -184,14 +184,14 @@ 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"
     | RApp          _ _ _ _ _ _ _     => "App"
-    | RLet          _ _ _ _ _ _ _     => "Let"
-    | RWhere        _ _ _ _ _ _ _ _   => "Where"
-    | RJoin         _ _ _ _ _ _ _     => "RJoin"
+    | RCut          _ _ _ _ _ _ _ _   => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
@@ -220,7 +220,8 @@ Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with
     | RArrange _    _ _ _ _ _ r => nd_hideURule r
     | RVoid _  _ _         => true
-    | RJoin _ _ _ _ _ _ _ => true
+    | RLeft _ _ _ _  _ _         => true
+    | RRight _  _ _ _ _ _        => true
     | _                         => false
   end.