            Installing then Certified Bsmllib library on a Unix machine
            -----------------------------------------------------------

PREREQUISITES
-------------

* The Objective Caml language version 3.00 or higher is required with native-code compilation (see next).
   (available at htpp://caml.inria.fr)

* The Coq Proof Assistant version 7.3.1 with native-code (see next).
    (available at htpp://coq.inria.fr)

* The Coqdoc software (http://www.lri.fr/~filliatr/coqdoc/index.en.html)




INSTALLATION INSTRUCTIONS
-------------------------

From the top directory, do:

        ./make

You can now used the Certified Bsmllib library. This will create the
following things:

doc/report/report.ps doc/report/report.pdf
          Technical report which explain this development.

doc/lib/BSML_COQ.htm
          html page of the Coq's development

src/*.vo
	the Certified Bsmllib modules for proofs

from_extraction/*.ml
	The programs extracted for the Coq's development	

Certified_library/lib/index.html
	 html page of the Certified Bsmllib library
	 
Certified_library/src/*.cmo
	Code modules of the Certified Bsmllib library (sequential simulo)
	
Installation is complete. Time to clean up. From the toplevel
directory, do "make clean".



COMMON PROBLEMS:
---------------

if you do not have native-compilation, remove "-opt" on the "Makefile" file
and change "ocamlc.opt" to "ocamlc" in the "Certified_library/src/Makefile" file.

Good By.
