Fixed: was using compare in place of eta_eq

in particular, eta_eq ignores arities of variables

there used to be cases of duplicate entries in PS (up to arities of variables)

(cherry picked from commit 79e9bd64d15490dd5abc353cc5b09378d3c640d1)

Re-use Util.index_of

(cherry picked from commit 52947a60467ebb10cec57ffc1725644ad605c671)

Code clean-up

Less casts and casts in the right place

(cherry picked from commit 6bf723ba426a04a3ae5d36baf8a9fe4bffebc635)

Tidying up problems.ml

(cherry picked from commit c8d9c2fda6b135b29e81e3bea95520ba449b86e3)

Tentative commit: tactics dropped and clean-up

(cherry picked from commit 0991fc5486c3158fc361e84cbba5aefa67893ba4)

Include codice di pure.ml che implementa Pure.B da commit
 "Removed bomb variable"

Added assert false

(cherry picked from commit ba6f0ecd9531b266361674d76423c24381dc72ee)

Fixed bug in eta_subterm

(cherry picked from commit 09ecd6ebdb7d96386bd79a7117930aba4635f778)

Remove FORCE option in Makefile

(cherry picked from commit 6ba14f58fa4c8f93fc2a398bdee030cd2217adea)

Fix: missing check to avoid stepping on vars of non positive arity

(cherry picked from commit 58f1518398346a81ccd8d0b14a14565b8bff5276)

Fix: max_arity_tms was using wrong comparison

(cherry picked from commit a104858f2dd754e5d086c3884823f3f39d716691)

Added variable convergent_dummy

Fixes to printing

(cherry picked from commit 4627d2b89b5a96e09b1921e033a5c1d7dd50dbc6)

Disabled some chars as variable names in the parser

(cherry picked from commit bfd8f8a98a7392ac8cbd9070a8e4ff4d06e09510)

Prettier-printing: string_of_problem outputs OCaml code

(cherry picked from commit d97b1a852472085bf3449e34f3b25aee349686fd)

Fixed if-then-else

(cherry picked from commit 588a00cd5ae861a2f366df992f758f285265a34a)

Fix: nested `Lambda(false,_) were not handled correctly

(cherry picked from commit 0147bacbe2db4055ae6f991aaa64a9fb1047edc6)

-666 -> min_int

(cherry picked from commit 5da7cf1322998c8965455264249f12ac4400f49d)

Fixed indentation and logging

(cherry picked from commit 4985769db038aa060b47ab40f673aaaacea54742)

clean removes *.o files

Removed old .ar files

Run tests with: make run

Fix: conv : x:min_int (.... y:1 ...)  y was not considered for stepping

When no other choice is available, step on any >0 variable that occurs in
a conv.

New problems n1, n2 used to debug the problem with dangerous variables fixed in the last commits

Bug fix: x (y z) where y was conv_dangerous did not make x so

Additional fix to last commit: args' where no longer checked for dangerous
variables. Fixed by passing three arguments to dangerous_invert_conv in
place of two.

Fix bug in dangerous_conv with arity of arguments of matches.
Next bug: variable replaced twice

The measure finally works on all problems in problems.ml!
Added in logs/fail.txt a fragment of a failing problem

Experimenting with a combined measure

Instantiate now uses a global initialSpecialK (ignoring the local one)
This fixes the bug in the previous commit, and makes the problem pass

Arity inherited only in the case (true, min_int)
Problem 25 fails because a fake variable becomes
critical step.

new_arity = old_arity + 1

Fixes to how arities are assigned and propagated
- added truelam to subst (useless, can be removed)
- TODO: to measure the problem, count the `fake` variables
        which are the ones with arity = min_int

Minor fixes

still stepping on negative variables

Problems pass, but still missing computation of arities of fresh applicative vars

New representation of arities in variables

Removed traces of lambda3

Removed lambda3 + Fixed lambda4

Updated type of terms with arities in lambda and matche

Moved andrea's stuff to its branch

Copy ocaml folder from sacerdot's svn repository, rev 4907

Initial commit