X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtractionMain.v;h=2f46f857e180e1fdcb1e1a754a6453ec6cbdd900;hb=5929a28895c9e8a12f3b60abf024a455ebe11e4c;hp=02643e5049ecabf15e3709568526e1b3e00c4acb;hpb=e83fd6f566ed0a7aaff19d67c2c2b64d08f98f7c;p=coq-hetmet.git

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 02643e5..2f46f85 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -33,13 +33,8 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
-Require Import ProgrammingLanguage.
-
 Require Import HaskProofFlattener.
 Require Import HaskProofStratified.
-Require Import HaskProofCategory.
-
-Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -118,7 +113,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 +132,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+++