CONTENTS:
========

Coq experiments around high-order refinement 
see http://www-lsr.imag.fr/Les.Personnes/Sylvain.Boulme/horefinement/
and the report "horef.ps.gz" at this url.

Coq version (coqc -v) :
The Coq Proof Assistant, version 8.1 (Feb. 2007)
compiled on fv 10 2007 20:29:26

The coq library for higher-order imperative specifications is in DSL directory.
(see LIST_OF_EXAMPLES inside).

Others directories:

SB_INIT (coq files): my personal "standard library"

MONADS \& REFINEMENT (coq files): 
a description of the algebraic semantics (see the report) using Coq modules. 
These directories are deprecated.

SCRIPT: dummy personal scripts (needed by makefiles).

See dependencies in Makefile.

COMPILATION (using "coqc"):
===========
  "make"  (take several minutes)
or
  "make <dir>"  in order to only compile <dir>
or 
  "cd <dir> ; make <file.vo>" in order to only compile <dir/file.v>

"make clean" to undo compilation.

ACKNOWLEDGMENT:
==============
 Jean-Christophe Fillitre reported me a very stupid mistake in my
 previous definition of permutations in SB_INIT/Array.v.
