update Demo.hs

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

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 5b73a41..9ec126e 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -8,7 +8,8 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
 
 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
@@ -46,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      *)
@@ -65,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!!! *)