OCaml Light for Coq Extraction

Revival of OCaml Light definition and formal semantics for Coq, for use in verified extraction in MetaCoq.

Dependencies

The easiest way to install the dependencies is via OPAM:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install ott coq-ott

Then, run make to generate and check all definitions.

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
theories		theories
.gitignore		.gitignore
.travis.yml		.travis.yml
Makefile		Makefile
Makefile.coq.local		Makefile.coq.local
README.internal		README.internal
README.md		README.md
README.ott		README.ott
_CoqProject		_CoqProject
coq-ocaml-light.opam		coq-ocaml-light.opam