Add Proofview.tclWRAPFINALLY

This new primitive (which could be implemented in terms of `tclCASE`,
but which I believe encapsulates a useful unit of behavior) is needed
for correctly implementing both `with_strategy` and for implementing
multi-success support for the Ltac Profiler.

The basic function of this tactical is to allow wrapping multi-success
tactics with initialization and cleanup routines.  For example, if `tac`
is a multi-success tactic that writes its status to a log file, you
might want to wrap `tac` in "first open the log file" and then after it
runs "finally close the log file".  (Unfortunately, the way the monad is
set up doesn't allow passing data from the most recent run of the
initializer to the tactic, which suggests that perhaps there's something
a bit off about this abstraction.  Perhaps we should set up a ref cell
and that will hold the most recent return of the initializer and pass
this ref cell to the wrapped tactic?  But this can be done externally
without needing to modify the current API.  In any case, such data is
not needed in the case of the Ltac Profiler, where the initializer is
"update the current call stack and record the current start time" and
the finalizer is "update the call stack and record the end time", and
you want to have the start time be restarted when re-entering a tactic.
Nor is it needed for `with_strategy` which needs to update the global
conv_oracle so that it plays nicely with `abstract`.)

0 files changed, 0 insertions, 0 deletions