X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionToLatex.v;fp=src%2FNaturalDeductionToLatex.v;h=1f6f32a8a6506b61277f02ff4050a5e8a4b695b8;hp=ddf6e8c94cee0d160da8a236d8ae1da08ef9a2f4;hb=148579e5c8f6b60209a442222b932cf59f163cca;hpb=6c06dcf3fee5a4f0c8f72c237de7bd30b7a2379b;ds=sidebyside

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