Documenting option -type-in-type.
Restoring non-uniform delta on local and global constants in 2nd order
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
Printing evar instance in a more intuitive order.
Merging some functions from evarutil.ml/evd.ml.

- Removed collect_evars which does not consider instance
  (use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
  evars_of_filterered_evar_info instead). This is consistent with
  printing goal contexts in the filtered way.
  Anyway, as of today, afaics goals filters are trivial
  because (if I interpret evarutil.ml correctly), evars with
  non-trivial filter necessarily occur in a conv pb. Conversely,
  conv pbs being solved when tactics are called, there should not be
  an evar used as a goal with a non-trivial filter.