blob: 5c6b788aa39d6e87f800588505e29c69e4e68398 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
(******************************************************************************)
(* *)
(* PROJECT HELM *)
(* *)
(* A module to print Coq objects in XML *)
(* *)
(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
(* 06/12/2000 *)
(******************************************************************************)
Declare ML Module "xml" "xmlcommand" "xmlentries".
Grammar vernac vernac : ast :=
xml_print [ "Print" "XML" tactic:qualidarg($id) "." ] ->
[(Print $id)]
| xml_print_file [ "Print" "XML" "File" stringarg($fn) tactic:qualidarg($id) "." ] ->
[(Print $id $fn)]
| xml_show [ "Show" "XML" "Proof" "." ] ->
[(Show)]
| xml_show_file [ "Show" "XML" "File" stringarg($fn) "Proof" "." ] ->
[(Show $fn)]
| xml_print_all [ "Print" "XML" "All" "." ] ->
[(XmlPrintAll)]
| xml_print_module [ "Print" "XML" "Module" identarg($id) "." ] ->
[(XmlPrintModule $id)]
| 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)].
|