Change log for the metatheory library

This log does not attempt to be exhaustive. Rather, it attempts to highlight the high-level changes that occurred between releases. The releases are listed from most recent to least recent.

2008-07-17 release

  • Not backwards compatible.
  • The finite sets implementation now uses directly 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. A separate signature specialized to atoms is provided.

Oregon Summer School 2008 release

  • Same as the 2007-07-16 release.

POPL 2008 Tutorial release

  • Not backwards compatible.
  • The files of the library were called out as such and generally "cleaned up."

Engineering Formal Metatheory release

  • The initial release of the library, in some sense. The components of the library were not really called out as such.