Formalisation de l'extraction de Coq en Coq
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Auteurs:
  Bruno Barras (LIX - École Polytechnique),
  Stéphane Glondu (PPS - Université Paris Diderot),
  Pierre Letouzey (PPS - Université Paris Diderot)

Ce développement a été testé avec Coq 8.2 et OCaml 3.10.2. Pour le
compiler, adaptez le Makefile et lancez "make".

 -- Stéphane Glondu <Stephane.Glondu@pps.jussieu.fr>  Tue, 14 Oct 2008 15:41:25 +0200
