diff options
| author | herbelin | 2001-09-20 15:44:31 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-20 15:44:31 +0000 |
| commit | 24c0e99bbe0ad4249df41f784ff4051599dd44cd (patch) | |
| tree | 0918b5ab71fa957f425f837fd7de7342c4b4032e /contrib/xml/Xml.v | |
| parent | 9c5ea6376c22187e1185e187e140d5c1765305c2 (diff) | |
Report des modifs de Claudio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2024 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/Xml.v')
| -rw-r--r-- | contrib/xml/Xml.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v index f1d91371e9..91fe6295ab 100644 --- a/contrib/xml/Xml.v +++ b/contrib/xml/Xml.v @@ -33,10 +33,10 @@ Grammar vernac vernac : ast := | xml_print_all [ "Print" "XML" "All" "." ] -> [(XmlPrintAll)] -| xml_print_module [ "Print" "XML" "Module" identarg($id) "." ] -> +| xml_print_module [ "Print" "XML" "Module" tactic:qualidarg($id) "." ] -> [(XmlPrintModule $id)] -| xml_print_module_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) identarg($id) "." ] -> +| xml_print_module_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) tactic:qualidarg($id) "." ] -> [(XmlPrintModule $id $dn)] | xml_print_section [ "Print" "XML" "Section" identarg($id) "." ] -> |