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.

1 files changed, 8 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 013b2f2047..49615a5f88 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -774,6 +774,11 @@ module V82 = struct
     Proof.put (b,([],[]))
 
   let catchable_exception = catchable_exception
+
+  let wrap_exceptions f =
+    try f ()
+    with e when catchable_exception e -> let e = Errors.push e in tclZERO e
+
 end
 
 
@@ -845,6 +850,9 @@ module Goal = struct
 
   (* compatibility *)
   let goal { self=self } = self
+  let refresh_sigma g =
+    tclEVARMAP >= fun sigma ->
+    tclUNIT { g with sigma }
 
 end