X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionToLatex.v;h=1f6f32a8a6506b61277f02ff4050a5e8a4b695b8;hp=ddf6e8c94cee0d160da8a236d8ae1da08ef9a2f4;hb=b096aab78240e38ff69c120367e65be60cbc54f5;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v
index ddf6e8c..1f6f32a 100644
--- a/src/NaturalDeductionToLatex.v
+++ b/src/NaturalDeductionToLatex.v
@@ -30,7 +30,6 @@ Section ToLatex.
 
     Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath :=
       match pns with
-        | scnd_leaf   ht c pn            => SCND_toLatexMath pn
         | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2
         | scnd_weak     c                => rawLatexMath ""
         | scnd_comp ht ct c pns rule     => if hideRule _ _ rule