(******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* A tactic to print Coq objects in XML *) (* *) (* Claudio Sacerdoti Coen *) (* 22/11/1999 *) (******************************************************************************) This is the main directory of the coq-like pretty printer for cic terms exported in xml from Coq. Once compiled four different executables are made: experiment a command-line pretty-printer (interpreted) experiment.opt same as experiment (compiled) gtkInterface a gtk-based pretty-printer (interpreted) gtkInterface.opt a gtk-based pretty-printer (compiled) To use one of the previous pretty-printer the syntax is pretty_printer_name file1 ... filen where filei is an xml cic object Code files: cic.ml the internal definition of cic objects and terms getter.ml converts uris to filenames retrieving the correspondent file cache.ml a cache for cic objects (actually a simple hash-table) cicParser.ml a parser from xml to internal definition: top level cicParser2.ml a parser from xml to internal definition: objects level cicParser3.ml a parser from xml to internal definition: terms level cicPp.ml a pretty-printer for the internal definition of cic objects experiment.ml a textual interface to cicPp gtkInterface.ml a gtk interface to cicPp Interface files: cache.mli getter.mli cicPp.mli cicParser.mli cicParser2.mli cicParser3.mli Other files: Makefile the targets are "all" "opt" "depend" "clean" .depend dependencies file used by make examples symbolic link to the root of the exported library