Reimplement conversion modulo AC

[fblanqui]

This PR reimplements conversion modulo AC without enforcing terms to be in AC-canonical form.
This is much more efficient but may not work with any rewrite system (fix #1200).
It seems to work well with:

• the theory ACI = AC + Idempotence used in max-suc algebra for universe levels,
• the theory of commutative groups AG = AC + Inverse + Neutral used in linear arithmetic.

CHANGES:

• main changes are in term.ml and eval.ml
• Logger.set_debug_in: use string argument instead of char + permute arguments
• Print: rename without_qualifying into no_qualif
• List: add rev_append2
• Term: add type side = Left | Right, used in properties and rewrite tactic
• Term: remove property Assoc
• when declaring a symbol as associative commutative, a side must be given now

TODO:

• do not declare term as private and remove functions mk_
• handle commutativity alone, fix tests/OK/ac.lp
• fix compute
• in applications, compare arguments from left to right
• try improve eq_modulo further
• update CHANGES
• update doc, add links to examples
• Logger.set_debug: permute arguments?

[fblanqui]

@NotBad4U Could you please try this PR on some other examples for linear arithmetic ?

[fblanqui]

Be careful that I changed the ordering: arguments are now compared from left to right. So, you need to permute the arguments of var.