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

diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v
index 66c1a5c..2d6fb55 100644
--- a/src/NaturalDeductionToLatex.v
+++ b/src/NaturalDeductionToLatex.v
@@ -9,10 +9,6 @@ Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import NaturalDeduction.
 
-(* string stuff *)
-Variable eol : string.
-Extract Constant eol  => "'\n':[]".
-
 Section ToLatex.
 
   Context {Judgment : Type}.
@@ -57,6 +53,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 +62,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 +70,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