aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/xml_parser.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/xml_parser.mli')
-rw-r--r--lib/xml_parser.mli4
1 files changed, 1 insertions, 3 deletions
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index e3e7ac4dc..2c83eee9d 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -27,9 +27,7 @@
(** An Xml node is either
[Element (tag-name, attributes, children)] or [PCData text] *)
-type xml =
- | Element of (string * (string * string) list * xml list)
- | PCData of string
+type xml = Serialize.xml
(** Abstract type for an Xml parser. *)
type t