Temporary fix: signature constants cannot match n[0-9]+
In a future version, this kind of overlap should simply be disallowed
Resolves #19
Update the case tactic for backchaining sequents

Previously it would always produce a member assumption.
Now it eagerly traverses the context and makes new cases for every
element of the context.
This might break existing proofs. To be tested.
Revert "Update the case tactic for backchaining sequents"

This breaks too many existing proofs and should be postponed to 2.1 or later.

This reverts commit 96fce26514b8e07567f949395f8570134a26631d.
In exists tactic, avoid name capture of other variables in the same quantifier.

Fixes #22
normalize_binding needs to accumulate the bound variables in its recursive case

This function has now been replaced by a much simpler and direct implementation
of the intuitive sense of renaming to avoid capture.

Fixes #23
Fixed a bug about raising over nominal constants.

When a goal formula G in {L |- G} is proved by backchaining
on some clause F in L or in the program. The clause F should
be raised over all nominal constants in {L |- G} instead of only
those in G.

As an example, the following judgment cannot be proved by Abella
before the fix,

   {of n1 (arr n2 T), of n3 n2 |- of (app n1 n3) T}

where the definition for 'of' is as follows:

   of : tm -> ty -> o.
   of (app M N) T :- of M (arr T1 T), of N T1.

This is because M, N, T1 are raised over n1,n3, but not n2.
As a result, the backchaining produces two subgoals

  {of n1 (arr n2 T), of n3 n2 |- of n1 (arr (T1' n1 n3) T)}
  {of n1 (arr n2 T), of n3 n2 |- of n3 (T1' n1 n3)}

Neither can be proved.

After the bug fix, the backchaining produces the following subgoals

  {of n1 (arr n2 T), of n3 n2 |- of n1 (arr (T1' n1 n2 n3) T)}
  {of n1 (arr n2 T), of n3 n2 |- of n3 (T1' n1 n2 n3)}

which can be proved by instantiating T1' with (x\y\z\ y).
More clear comments
The 'clause_aux' function backchains G in {L |- G} on some clause in
L or in the program. It never uses the hypotheses.
Add support for unfold <n>.

Semantics:

 - Plain "unfold" still means: first clause that matches
 - New "unfold n" means:
   - check that the definition has at least n clauses
     (error otherwise)
   - then attempt to unfold only the nth clause

Clauses are numbers from 1 to total number of clauses in that mutually
(co)inductive definition group.

Resolves #5.
Normalize goal after existential instantiation.

Fixes #24.
normalize_binders: used variables need to be always extended for binders

Fixes a lingering issue with #23.
Proof for the meta-theory of HH
Updated the index page of the examples
Support for merlin-mode

http://kiwi.iuwt.fr/~asmanur/blog/merlin/