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