Declare ML Module "iXml" "xmltheoryentries".

(*Vecchio, ma funzionante
Grammar vernac vernac : ast :=
  xml_theory_begin [ "XmlTheory" "Begin" stringarg($s) stringarg($f) "." ] ->
     [(XMLTHEORYBEGIN $s $f)]
| xml_theory_end [ "XmlTheory" "End" "." ] ->
     [(XMLTHEORYEND)].
*)

Grammar vernac vernac : ast :=
  xml_theory_begin [ "XmlTheory" "Begin" identarg($s) stringarg($f) "." ] ->
     [(XMLTHEORYBEGIN $s $f)]
| xml_theory_end [ "XmlTheory" "End" "." ] ->
     [(XMLTHEORYEND)].