Debugging stuff removed.

[helm.git] / helm / interface / README

diff --git a/helm/interface/README b/helm/interface/README
index 89265ca8aa2f6134db42db751e7739fb8fd77a8c..63d2c2ac84e879a6672476e9033af689cc538e78 100644 (file)
--- a/helm/interface/README
+++ b/helm/interface/README
@@ -1,44 +1,8 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A tactic to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 22/11/1999                                 *)
-(******************************************************************************)
+NOTE: This is the first alpha release of project HELM.
 
-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:
+HELM (Hypertextual Electronic Library of Mathematics) is a project aimed
+at the creation of tools for the development and exploitation of a huge
+distributed library of formal mathematical knowledge. This package holds
+a gtk interface to the library.
 
- 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
+For more information see http://www.cs.unibo.it/helm