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

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}.