X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction.v;fp=src%2FExtraction.v;h=d04df843643b3d90000997bb69e088e619bace58;hp=65f3f2d144b10cc56a49fac75d8ae99492dcf490;hb=0126c02cc846952aa847660475e88a152c9a2574;hpb=10713ada476b463a3b25ffd0f0f17315f5fd72a3

diff --git a/src/Extraction.v b/src/Extraction.v
index 65f3f2d..d04df84 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -68,11 +68,11 @@ Section core2proof.
   Definition Δ : CoercionEnv Γ := nil.
 
   Definition φ : TyVarResolver Γ :=
-    fun cv => (fun TV env => Prelude_error "unbound tyvar").
+    fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
 
-  Definition ψ : CoreVar->HaskCoVar nil Δ
-    := fun cv => Prelude_error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
+  Definition ψ : CoVarResolver Γ Δ :=
+    fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
 
   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
    * free tyvars in them *)