From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 14 Mar 2011 08:45:36 +0000 (-0700)
Subject: move eol:string to General.v
X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=3b5653626dbeb9eb554112527ff0a70b369c6a6a;p=coq-hetmet.git

move eol:string to General.v
---

diff --git a/src/General.v b/src/General.v
index 7af1fc3..457b421 100644
--- a/src/General.v
+++ b/src/General.v
@@ -629,6 +629,10 @@ CoInductive Fresh A T :=
 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 
 
+(* string stuff *)
+Variable eol : string.
+Extract Constant eol  => "'\n':[]".
+
 
 (* the Error monad *)
 Inductive OrError (T:Type) :=
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}.