X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionToLatex.v;fp=src%2FNaturalDeductionToLatex.v;h=34f289400037e260517c0ef26032a710878fece1;hp=66c1a5cd6b03ad5e342fc0072cbd91550cc7c468;hb=ee7da23597402df671f18320edff6604f5f6de7c;hpb=112daf37524662d6d2267d3f7e50ff3522683b8f

diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v
index 66c1a5c..34f2894 100644
--- a/src/NaturalDeductionToLatex.v
+++ b/src/NaturalDeductionToLatex.v
@@ -57,6 +57,8 @@ Section ToLatex.
 
   (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
   Section SCND_toLatex.
+
+    (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
     Context (hideRule : forall h c (r:Rule h c), bool).
 
     Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
@@ -64,7 +66,6 @@ Section ToLatex.
         | scnd_leaf   ht c pn            => SCND_toLatex pn
         | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2
         | scnd_weak     c                => ""
-        | scnd_axiom c               => judgment2latex c +++ eol
         | scnd_comp ht ct c pns rule => if hideRule _ _ rule
                                       then SCND_toLatex pns
                                       else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
@@ -73,7 +74,7 @@ Section ToLatex.
       end.
   End SCND_toLatex.
 
-  (* FIXME: this doesn't actually work properly (but SCND_toLatex does!) *)
+  (* this is a work-in-progress; please use SCND_toLatex for now *)
   Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
     match nd with
       | nd_id0                      => indent +++ "% nd_id0 " +++ eol