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.

2 files changed, 16 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
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index fed7c1dfd9..021155c425 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -333,6 +333,10 @@ module V82 : sig
   (* exception for which it is deemed to be safe to transmute into
      tactic failure. *)
   val catchable_exception : exn -> bool
+
+  (* transforms every Ocaml (catchable) exception into a failure in
+     the monad. *)
+  val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
 end
 
 (* The module goal provides an interface for goal-dependent tactics. *)
@@ -370,6 +374,10 @@ module Goal : sig
 
   (* compatibility: avoid if possible *)
   val goal : t -> Goal.goal
+
+  (** [refresh g] updates the [sigma g] to the current value, may be
+      useful with compatibility functions like [Tacmach.New.of_old] *)
+  val refresh_sigma : t -> t tactic
 end
 
 (* The [NonLogical] module allows to execute side effects in tactics