1 (******************************************************************************)
5 (* A tactic to print Coq objects in XML *)
7 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
9 (******************************************************************************)
11 This is the main directory of the coq-like pretty printer for cic terms exported
12 in xml from Coq. Once compiled four different executables are made:
14 experiment a command-line pretty-printer (interpreted)
15 experiment.opt same as experiment (compiled)
16 gtkInterface a gtk-based pretty-printer (interpreted)
17 gtkInterface.opt a gtk-based pretty-printer (compiled)
19 To use one of the previous pretty-printer the syntax is
21 pretty_printer_name file1 ... filen
23 where filei is an xml cic object
27 cic.ml the internal definition of cic objects and terms
28 getter.ml converts uris to filenames retrieving the correspondent file
29 cache.ml a cache for cic objects (actually a simple hash-table)
30 cicParser.ml a parser from xml to internal definition: top level
31 cicParser2.ml a parser from xml to internal definition: objects level
32 cicParser3.ml a parser from xml to internal definition: terms level
33 cicPp.ml a pretty-printer for the internal definition of cic objects
34 experiment.ml a textual interface to cicPp
35 gtkInterface.ml a gtk interface to cicPp
38 cache.mli getter.mli cicPp.mli cicParser.mli cicParser2.mli cicParser3.mli
42 Makefile the targets are "all" "opt" "depend" "clean"
43 .depend dependencies file used by make
44 examples symbolic link to the root of the exported library