diff options
Diffstat (limited to 'contrib/xml/Xml.v')
| -rw-r--r-- | contrib/xml/Xml.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v index 01461afbf8..d0737b3116 100644 --- a/contrib/xml/Xml.v +++ b/contrib/xml/Xml.v @@ -26,8 +26,14 @@ Grammar vernac vernac : Ast := | xml_print_all [ "Print" "XML" "All" "." ] -> [(XmlPrintAll)] -| xml_print_dir [ "Print" "XML" "Module" identarg($id) "." ] -> +| xml_print_module [ "Print" "XML" "Module" identarg($id) "." ] -> [(XmlPrintModule $id)] -| xml_print_dir_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) identarg($id) "." ] -> - [(XmlPrintModule $id $dn)]. +| xml_print_module_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) identarg($id) "." ] -> + [(XmlPrintModule $id $dn)] + +| xml_print_section [ "Print" "XML" "Section" identarg($id) "." ] -> + [(XmlPrintSection $id)] + +| xml_print_section_disk [ "Print" "XML" "Section" "Disk" stringarg($dn) identarg($id) "." ] -> + [(XmlPrintSection $id $dn)]. |