I've just released Abella 1.3.5. The new version is available at
http://abella.cs.umn.edu/ and a detailed list of changes follows:
* The apply and backchain tactics now produce witnesses when the
witnesses option is enabled.
* The unfold tactic applied using a definition with nabla in the head
will now use "dummy nominals" in case the nabla bound variables are
not used.
* / can no longer begin a name.
* Underscore can now be used to represent anonymous variables in
lambdaProlog specifications.
* Fixed a bug when using apply with no arguments.
* Fixed a bug in the normalization of binder names
-Andrew