+++ /dev/null
-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)].