]> matita.cs.unibo.it Git - helm.git/blob - helm/xmltheory/XmlTheory/XmlTheory.v
removed an ancient debugging message
[helm.git] / 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)].