X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FGeneral.v;h=e1e57910bb30a4ea3160927b3767bb1df800cf28;hb=30cc675d57492799644506f3632625f371a3e89a;hp=7e0af438ef4197e432ef9fb55615e239082b8240;hpb=693c6f552555f14c085a71e0b03c67d3c051eaa1;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index 7e0af43..e1e5791 100644
--- a/src/General.v
+++ b/src/General.v
@@ -129,7 +129,14 @@ Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
     reflexivity.
     Qed.
 
-
+Open Scope string_scope.
+Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
+match t with
+  | T_Leaf None => "[]"
+  | T_Leaf (Some s) => "["+++s+++"]"
+  | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
+end.
+Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
 
 (*******************************************************************************)
 (* Lists                                                                       *)
@@ -717,3 +724,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".