blob: 01461afbf8b55a38e1b2195f3d4ca05abc9c6630 (
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
|
(******************************************************************************)
(* *)
(* PROJECT HELM *)
(* *)
(* A tactic to print Coq objects in XML *)
(* *)
(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
(* 17/11/1999 *)
(******************************************************************************)
Declare ML Module "xml" "cooking" "xmlcommand" "xmlentries".
Grammar vernac vernac : Ast :=
xml_print [ "Print" "XML" identarg($id) "." ] ->
[(Print $id)]
| xml_print_file [ "Print" "XML" "File" stringarg($fn) identarg($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_dir [ "Print" "XML" "Module" identarg($id) "." ] ->
[(XmlPrintModule $id)]
| xml_print_dir_disk [ "Print" "XML" "Module" "Disk" stringarg($dn) identarg($id) "." ] ->
[(XmlPrintModule $id $dn)].
|
