X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=f7f47a35e2745f0993f5dd364ec543aadb888c5e;hp=02643e5049ecabf15e3709568526e1b3e00c4acb;hb=c3b1fb9622a65ad01e54b6e35785cee672d25bdc;hpb=6133ffc255c4cfadf93378b93ddd43adf0787120

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 02643e5..f7f47a3 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -37,7 +37,6 @@ Require Import ProgrammingLanguage.
 
 Require Import HaskProofFlattener.
 Require Import HaskProofStratified.
-Require Import HaskProofCategory.
 
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
@@ -118,7 +117,7 @@ Section core2proof.
     "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
     "\usepackage[tightpage,active]{preview}"+++eol+++
     "\begin{document}"+++eol+++
-    "\setlength\PreviewBorder{5pt}"+++eol+++.
+    "\setlength\PreviewBorder{5pt}"+++eol.
 
   Definition footer : string :=
     eol+++"\end{document}"+++
@@ -137,7 +136,7 @@ Section core2proof.
                   addErrorMessage ("HaskType: " +++ toString τ)
                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
                     OK (eol+++eol+++eol+++
-                        "\begin{preview}"+++eol
+                        "\begin{preview}"+++eol+++
                         "$\displaystyle "+++
                         toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
                         " $"+++eol+++