X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtraction.v;h=53b1185cd5934ff8883d411b477987795f8c457f;hb=601b57023dd6fe4295c5af8bb3f5c508618a5f64;hp=dfca44c27bbf5b23e9971b09267f23ef3b8852a1;hpb=f6732490f83e19174b8a8a6b487da95913d9f02d;p=coq-hetmet.git

diff --git a/src/Extraction.v b/src/Extraction.v
index dfca44c..53b1185 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -12,7 +12,7 @@ Require Import NaturalDeduction.
 Require Import NaturalDeductionToLatex.
 
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -58,8 +58,6 @@ Extract Constant shift  => "shiftAscii".
 Unset Extraction Optimize.
 Unset Extraction AutoInline.
 
-Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
-
 Section core2proof.
   Context (ce:@CoreExpr CoreVar).
 
@@ -78,7 +76,7 @@ Section core2proof.
    * free tyvars in them *)
   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
     match coreVarToWeakVar cv with
-      | WExprVar wev => match weakTypeToType'' φ wev ★ with
+      | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
                           | Error s => Prelude_error ("Error in top-level xi: " +++ s)
                           | OK    t => t @@ nil
                         end
@@ -91,10 +89,10 @@ Section core2proof.
     "\usepackage{amsmath}"+++eol+++
     "\usepackage{amssymb}"+++eol+++
     "\usepackage{proof}"+++eol+++
-    "\usepackage{mathpartir}"+++eol+++
-    "\usepackage{trfrac}"+++eol+++
+    "\usepackage{mathpartir}   % http://cristal.inria.fr/~remy/latex/"+++eol+++
+    "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
-    "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
+    "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
     "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
     "\begin{document}"+++eol+++
     "\begin{preview}"+++eol.
@@ -112,7 +110,7 @@ Section core2proof.
           ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
             ((weakTypeOfWeakExpr we) >>= fun t =>
               (addErrorMessage ("WeakType: " +++ t)
-                ((weakTypeToType'' φ t ★) >>= fun τ =>
+                ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
                   addErrorMessage ("HaskType: " +++ τ)
                   ((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e =>
                     OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)