X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakTypes.v;h=9ec126eb69607f52924330adbc336a62133d5870;hp=9b34188909466177ebad0480def137c84d070343;hb=14afe39e905be69eabd8944b97bb2b731bf44939;hpb=f9fa41bde5a3df1037b0b153ead92bb016ba9613

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 9b34188..9ec126e 100644
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -47,7 +47,7 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
     Defined.
 
 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
-Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
 
 Inductive WeakCoercion : Type :=
 | WCoVar          : WeakCoerVar                                   -> WeakCoercion (* g      *)
@@ -66,7 +66,7 @@ Inductive WeakCoercion : Type :=
 
 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
 match wc with
-| WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
+| WCoVar     (weakCoerVar _ t1 t2)   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoType    t                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoApp     c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoAppT    c t                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)