From 3b5653626dbeb9eb554112527ff0a70b369c6a6a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 01:45:36 -0700 Subject: [PATCH] move eol:string to General.v --- src/General.v | 4 ++++ src/NaturalDeductionToLatex.v | 4 ---- 2 files changed, 4 insertions(+), 4 deletions(-) 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}. -- 1.7.10.4