Tacinterp: fewer Proofview.Goal.enterl.

I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their
context.

Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API).

Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way).

Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.

0 files changed, 0 insertions, 0 deletions