Change log for the metatheory library
This log does not attempt to be exhaustive list of every single change. Rather, it highlights the high-level changes that occurred between releases. The releases are listed in reverse chronological order.
20090321
- This is the first version to support Coq 8.2. Due to changes in Coq's FSets library, previous versions of Coq are no longer supported.
-
The AtomSet library reflects changes to Coq's FSets library. The
tactics defined here (e.g.,
atomsetdec
) have been renamed in an attempt to more consistently name things. -
The FSetWeakNotin library now supports the
remove
operation. - The ListFacts library has been simplified by removing apparently unneeded lemmas.
- The levels for some notations have changed.
oregon08-tutorial
- Finite sets are now implemented directly using Coq's FSets library. We no longer wrap the FSets library with an additional axiom about extensional equality. In practice, it seems that the lemma is unnecessary. Setoid rewriting seems to be sufficient.
- The library for environments is now implemented as a generic library about association lists (AssocList). A separate signature specialized to atoms is provided (AtomEnv).
popl08-tutorial
- Code was substantially tweaked and reorganized for pedagogical reasons.
- The only examples included now are STLC (simply typed lambda calculus) and Fsub (System F with subtyping).
- The distribution now includes an introduction to using Coq.
popl08-paper
- The initial release of the library.