Move the handling a new evars from the [Proofview.Refine] module to [Evd].

That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct.

It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though.

Following a suggestion by Hugo.

0 files changed, 0 insertions, 0 deletions