X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakTypes.v;h=5b73a41ae629278e8ae8912eaa93d1428354af2c;hp=4d6500d5607d0fb0debcae08a7ef63c3468df510;hb=786b693ac8d5f2081db75b49bba838a6cff7e2f6;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 4d6500d..5b73a41 100644
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -63,18 +63,17 @@ Inductive WeakCoercion : Type :=
 (*| WCoTFApp        : ∀ n, TyFunConst n -> vec WeakCoercion n       -> WeakCoercion (* S_n γⁿ *)*)
 .
 
-Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
 match wc with
 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
-| WCoType    t                       => Prelude_error "FIXME WCoType"
-| WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
-| WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
-| WCoAll     k f                     => Prelude_error "FIXME WCoAll"
+| WCoType    t                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoApp     c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoAppT    c t                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoAll     k f                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
-| WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
-| WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
-| WCoRight   c                       => Prelude_error "FIXME WCoRight"
+| WCoComp    c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoLeft    c                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoRight   c                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoUnsafe  t1 t2                   => (t1,t2)
 end.