Proof for the meta-theory of HH
Updated the index page of the examples
Fixed the syntax of plugins command (pure and pure_top) to be DOT terminated
factored recursePPOn and recursePOn out of process and together as instances of recurseP
fixed A. M.'s bug where the first call to recurseOn while in interactive mode would stop the prover
Schema.process_tactic and Schema.process_top should now undo their work, print an error message and return unit, instead of exiting abella, if an exception is raised BEFORE using the call-back function. Failures within the call-back function (Abella.recurseOn) still provoke an exit, after printing a message asking the unlucky user to report the bug to the issue tracker.
Support for merlin-mode

http://kiwi.iuwt.fr/~asmanur/blog/merlin/
Typing support for spec-level and.

No support for it at the reasoning level currently.
Fixed printing of warning when a tacticals cannot be applied
Reasoning support negative occurrences of & in object sequents.

At runtime, any encounter with a positive & results in the error
message:  "Abella does not support & in clause heads or goals".

Note that this cannot be checked entirely statically as users
can happily do whatever they want using variables of type o
at the reasoning level.
Merge branch 'spec-and' into schemas
updated schemaparser to accept &-terms