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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 02643e5..49be891 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.
+(*Require Import HaskProofFlattener.*)
+(*Require Import HaskProofStratified.*)
 
 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+++