major revision of HaskWeakToStrong, put phi/psi on the error monad

[coq-hetmet.git] / src / Extraction.v

diff --git a/src/Extraction.v b/src/Extraction.v
index 65f3f2d..d04df84 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -68,11 +68,11 @@ Section core2proof.
   Definition Δ : CoercionEnv Γ := nil.
 
   Definition φ : TyVarResolver Γ :=
   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)).*)
 
     (*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 *)
 
   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
    * free tyvars in them *)