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.

0 files changed, 0 insertions, 0 deletions