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

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).