################################################################################
#                                                                              #
#                       The Certified BSMLlib 0.2pre                           #
#                                                                              #
################################################################################

By Frdric Gava


CONTENTS:
---------

INSTALL               instructions for installation
README                this file
doc/		      documentations
   lib/                   html of the "Coq Proof Assistant" code source
   report/                Technical report of the Certified Library (explain Coq's source)

src/	              the certified bsmllib library in Coq
from_extraction/      programs given by the Coq's extraction program from the code source

Certified-Bsmllib/    the certified bsmllib library in Ocaml
      src/                 source of the certified library in Ocaml
      lib/                 html of the Ocaml code source


INSTALLATION:
-------------

See the file INSTALL for installation instructions on Unix machines.


DOCUMENTATION:
-------------

A technical report "report.ps" (or "report.pdf") is free available with 
this distribution. The Coq system is available at http://coq.inria.fr, the Ocaml
language at http://caml.inria.fr and The Bsmllib  at http://bsmllib.free.fr.

The Certified Bsmllib is exactly the Ocaml programs extracted from the Coq's source
with a sequential simulo, a certified arithmetic library (from the work of Pierre Casteran)
and without redundance of definitions (this bug will be remove in future Coq System versions).

The Certified Bsmllib is distributed in HTML and is free available on 
the World Wide Web, at http://univ-paris12.fr/lacl/gava


BUG REPORTS AND USER FEEDBACK:
-----------------------------

Send your bug reports by E-mail to:

 gava@univ-paris12.fr

To be effective, bug reports should include a complete program
(preferably small) that exhibits the unexpected behavior, and the
configuration you are using (machine type, etc).



LICENCE:
-------

Copyright (C) 2003, GavaSoft Inc. 
 9 rue Foubert 76130 Mont St Aignan ;-)

Good By.
