diff options
| author | pboutill | 2012-05-23 14:41:24 +0000 |
|---|---|---|
| committer | pboutill | 2012-05-23 14:41:24 +0000 |
| commit | 8837c2365c382adb0a74bfedabb1659eeb472adc (patch) | |
| tree | 88761584df9487ab39fe2bc2627c029d67acc229 /lib/xml_utils.ml | |
| parent | 24473ef1954c856907ba8907a4d2c910505125a1 (diff) | |
Revert copy/pasted function in to minilib thanks to clib.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/xml_utils.ml')
| -rw-r--r-- | lib/xml_utils.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml index 1d09b1723b..48ee546cad 100644 --- a/lib/xml_utils.ml +++ b/lib/xml_utils.ml @@ -24,17 +24,6 @@ exception Not_element of xml exception Not_pcdata of xml exception No_attribute of string -let default_parser = Xml_parser.make() - -let parse (p:Xml_parser.t) (source:Xml_parser.source) = - (* local cast Xml.xml -> xml *) - (Obj.magic Xml_parser.parse p source : xml) - -let parse_in ch = parse default_parser (Xml_parser.SChannel ch) -let parse_string str = parse default_parser (Xml_parser.SString str) - -let parse_file f = parse default_parser (Xml_parser.SFile f) - let tag = function | Element (tag,_,_) -> tag | x -> raise (Not_element x) |