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

diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v
index 34f2894..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}.