helm/xmltheory/XmlTheory/XmlTheory.v

   1 Declare ML Module "iXml" "xmltheoryentries".
   2
   3 (*Vecchio, ma funzionante
   4 Grammar vernac vernac : ast :=
   5   xml_theory_begin [ "XmlTheory" "Begin" stringarg($s) stringarg($f) "." ] ->
   6      [(XMLTHEORYBEGIN $s $f)]
   7 | xml_theory_end [ "XmlTheory" "End" "." ] ->
   8      [(XMLTHEORYEND)].
   9 *)
  10
  11 Grammar vernac vernac : ast :=
  12   xml_theory_begin [ "XmlTheory" "Begin" identarg($s) stringarg($f) "." ] ->
  13      [(XMLTHEORYBEGIN $s $f)]
  14 | xml_theory_end [ "XmlTheory" "End" "." ] ->
  15      [(XMLTHEORYEND)].