move Prelude_error to General.v

[coq-hetmet.git] / src / General.v

diff --git a/src/General.v b/src/General.v
index 7e0af43..100da75 100644 (file)
--- 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".