Small cleaning and uniformization in unification flags:

- new function set_flags_for_type for setting flags when converting
  types of the terms to unify
  - it now sets all conversion flags, possibly restricting delta using
    modulo_delta_types
  - it is now used in w_unify_core_0 too
- fixing/improving documentation of options
- deprecating "Set Tactic Evars Pattern Unification"
More printers in tracer.
Fix debugger Tactic Unification.