Initial revision

[helm.git] / helm / xmltheory / XmlTheory / XmlTheory.v

diff --git a/helm/xmltheory/XmlTheory/XmlTheory.v b/helm/xmltheory/XmlTheory/XmlTheory.v
new file mode 100644 (file)
index 0000000..54fdf82
--- /dev/null
+++ b/helm/xmltheory/XmlTheory/XmlTheory.v
@@ -0,0 +1,15 @@
+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)].