X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=323c1d66c4bbcae0019dcd12815fab98ae2d5bd2;hp=b787d3eaca3e2c70771f09e33b51dc45c30aa442;hb=6a7c6977507488245ba4b8cabcf323920c25baef;hpb=d9117c50c1e7d287651720b5cda988c8821b8d62;ds=sidebyside diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index b787d3e..323c1d6 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -190,7 +190,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" - | RCut _ _ _ _ _ _ _ => "Cut" + | RCut _ _ _ _ _ _ _ _ => "Cut" | RLeft _ _ _ _ _ _ => "Left" | RRight _ _ _ _ _ _ => "Right" | RWhere _ _ _ _ _ _ _ _ => "Where"