X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;fp=src%2FHaskWeakToStrong.v;h=c4e1873bfcfabd5c3a195c992cc3945124f20bdc;hp=aeb42b122d77dc61e00e93a98ccf321e6cd4d7e9;hb=f788a2864edbc5ba1ffb7ae5632fc3290f8febf1;hpb=132fd8b8ed861301b0ed38d286770003ea18396b

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index aeb42b1..c4e1873 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -224,9 +224,6 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply h.
     Defined.
     
-
-Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
-
 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 Section StrongAltCon.
   Context (tc : TyCon)(dc:DataCon tc).