X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=537bfbe0512a4817d6b489b0c23e6e654255035d;hp=31accd29a2e1dae3d03187191b76d13d94833e74;hb=8c26722a1ee110077968a8a166eb7130266b2035;hpb=b8f6adf700fa3c67feefaea3d2cf5c4626300489

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 31accd2..537bfbe 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -104,17 +104,17 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
     | WEApp   e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
                        match t' with
                          | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
-                         | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
+                         | _ => Error ("found non-function type "+++t'+++" in EApp")
                        end
     | WETyApp e t    => weakTypeOfWeakExpr e >>= fun te =>
                         match te with
                           | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
-                          | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
+                          | _ => Error ("found non-forall type "+++te+++" in ETyApp")
                         end
     | WECoApp e co   => weakTypeOfWeakExpr e >>= fun te =>
                         match te with
                           | WCoFunTy t1 t2 t => OK t
-                          | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
+                          | _ => Error ("found non-coercion type "+++te+++" in ETyApp")
                         end
     | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
     | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')