Internal extraction
~~~~~~~~~~~~~~~~~~~

Authors:

  SG = Stéphane Glondu (PPS - Université Paris Diderot)
  PL = Pierre Letouzey (PPS - Université Paris Diderot)
  ZD = Zaynah Dargaye (GALLIUM - INRIA Paris-Rocquencourt)

License:

  CeCILL 2.0 (http://www.cecill.info/), unless otherwise specified.

Tested with Coq 8.4beta and OCaml 3.12.1. To compile, run:

  make

Layout:

  Ml.v                    syntax of ML terms (adapted from ZD)
  MlSubstitutions.v       substitutions (SG+PL)
  MlSem.v                 two semantics of ML:
                          - big steps with environment (adapted from ZD)
                          - small steps with substitutions (SG)
                          - equivalence proof (mainly PL)
  MlSemExtra.v            additional definitions (SG)
  InternalExtraction.v    Coq infrastructure for internal extraction (SG)
  *.ml*                   plugin (SG, adapted from PL)
  Examples.v              examples (SG)

The file sandbox.el can give suggestions on how to run interactively
.v files inside Proof General.

 -- Stéphane Glondu <Stephane.Glondu@pps.univ-paris-diderot.fr>  Wed, 25 Jan 2012 11:35:58 +0100
