Abella 2.0.6

[Kaustuv Chaudhuri]

Abella version 2.0.6 is now officially released. As Yuting Wang has already mentioned on this list, the main new feature is that Abella now supports schematically polymorphic specifications, definitions, theorems, and proofs.

<http://abella-prover.org/distributions/abella-2.0.6.tar.gz>

As usual the easiest way to install Abella is to use

   opam install abella

Note that this release requires OPAM version 2.0 or later. You may need to upgrade your OPAM installation first. You can of course still compile and use Abella without OPAM by running "make". The minimum required version of OCaml (4.02.3) has not changed.

The list of changes is included below.

Kaustuv

----

Changes in 2.0.6 from 2.0.5
---------------------------

Additions

* The schematic polymorphism branch has been merged.

  You can read more about it here:

     http://abella-prover.org/schm-poly/index.html

  Thanks to Yuting Wang and Gopalan Nadathur for developing the theory
  to match the implementation by Yuting.


Tweaks to existing functionality

* Polymorphic definitions and theorems in the style of version 2.0.5
  are now recast in the style of schematic polymorphism in 2.0.6.
  There should be minimal user-visible impact.


Bugfixes

* Confusing nominal and other constants in eta-contraction
  #110 (Reported by Yuting Wang)
* Permutations of nominal constants in equivariant
  matching failed to respect types.
  #107 (Reported by Matija Pretnar)
* Error in renaming of bound variabls in metaterms.
  #106 (Reported by Yuting Wang)
* Incorrect pretty-printing of `(pi x\ p x)`.
  #104 (Reported by Dan DaCosta)