From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 19 Mar 2011 21:15:05 +0000 (-0700)
Subject: move Prelude_error to General.v
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=f788a2864edbc5ba1ffb7ae5632fc3290f8febf1

move Prelude_error to General.v
---

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