mattam82 (Matthieu Sozeau)

Typos, explain Constructors.v

Cleanup repo, leaving doc/intro.v to be expanded.

Move paper out of the sources repo.

Correct treatment of helper identifiers.

First almost final version (still comp on refinement nodes to define).

Add README

Move paper to new place for shortening.

Last fixes on slides, presentable now :)

Last rev of slides, complete with demo

by keyword, complete slides

New "with c :=" syntax, Below_vector won't check anymore due to guardness problem?

First rev of the slides.

Move to llncs and fix Fin defs.

- Update paper to new rec syntax

Use a correcness typeclass to index correctness lemmas, try to be more robust, not relying on simpl

binary_of_nat_be args in the right order again.

Compiles fully again, with new proofs using functional elimination and

Fix handling of recursion on packed objects.

Proper locations in error messages and proper variable names.

Cleanup the eliminator some more. The proof needs a bit more clever

Update to latest equations version, removed nasty False hint from the core

Basics compiles again, and strong enough eliminators are generated for all

Compile with the latest equations, use functional eliminators in

Sort patvars at refine nodes to avoid constructing ill-typed contexts.

Much better elimination principle that removes all the work of

Definitely fixed treatment of refined terms and remove hack with references.

Fix refine and better recognition of refined terms in proofs, Basics.v compiles

Finish recursion section, start experiments.

Support section.

Continue paper. Temporarily disable strengthening to accept more

Finish recursion section.

Continue paper, moving to recursion.

Update to trunk, start impl section of paper.