Fix a bug with with_strategy, behavior on multisuccess tactics

Copy tclWRAPFINALLY to tactics.ml

As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't export
it from Proofview, because it seems somehow not primitive enough.  But
we don't export it from Tactics because it is more of a tactical than a
tactic.  But we don't export it from Tacticals because all of the
non-New tacticals there operate on `tactic`, not `Proofview.tactic`, and
all of the `New` tacticals that deal with multi-success things are
focussing, i.e., apply their arguments on each goal separately (and it
even says so in the comment on `New`), whereas it's important that
`tclWRAPFINALLY` doesn't introduce extra focussing.

0 files changed, 0 insertions, 0 deletions