X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=f97989d2677f6c1cbafc6783ea70b1423901a9fc;hp=db77f344df6bf4e9361bf583700b048e2035fc56;hb=794719aadd55d760c0514f45c23b9cb450d92d9f;hpb=4a32fb619ddda1fedb0855a0c7acad0a41704da8

diff --git a/src/General.v b/src/General.v
index db77f34..f97989d 100644
--- a/src/General.v
+++ b/src/General.v
@@ -469,6 +469,15 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
   apply eqd_dec.
   Defined.
 
+Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string :=
+  match l with
+    | nil  => "nil"
+    | a::b => (toString a) +++ "::" +++ listToString b
+  end.
+
+Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
+  { toString := @listToString _ _ }.
+
 (*******************************************************************************)
 (* Tree Flags                                                                  *)