From f788a2864edbc5ba1ffb7ae5632fc3290f8febf1 Mon Sep 17 00:00:00 2001
From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 19 Mar 2011 14:15:05 -0700
Subject: [PATCH] move Prelude_error to General.v

---
 src/General.v          |    4 ++++
 src/HaskWeakToStrong.v |    3 ---
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/General.v b/src/General.v
index 7e0af43..100da75 100644
--- a/src/General.v
+++ b/src/General.v
@@ -717,3 +717,7 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     Defined.
 
 
+
+
+
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
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).
-- 
1.7.10.4