X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction.v;fp=src%2FExtraction.v;h=ae55381e2147cdfc5041ce6be3797b5fd33d91b4;hp=d83a937ac8e05750da60102ca753bfff38d9b887;hb=273645efdb974dd04042e6c59bbedbe0ad658298;hpb=72d3380355a80135c91e77736f1ebb6ca4f43923

diff --git a/src/Extraction.v b/src/Extraction.v
index d83a937..ae55381 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -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
@@ -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)