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.

1 files changed, 36 insertions, 0 deletions

diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index 4f761fb470..e0d0252a47 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -149,6 +149,42 @@ Proof using Type.
        reflexivity).
 Time Timeout 5 Qed.
 
+(* test that the strategy is correctly reverted after closing the goal completely *)
+Goal id 0 = 0.
+  assert (id 0 = 0) by with_strategy expand [id] reflexivity.
+  Fail unfold id.
+  reflexivity.
+Qed.
+
+(* test that the strategy is correctly reverted after failure *)
+Goal id 0 = 0.
+  let id' := id in
+  (try with_strategy expand [id] fail); assert_fails unfold id'.
+  Fail unfold id.
+  (* a more complicated test involving a success and then a failure after backtracking *)
+  let id' := id in
+  ((with_strategy expand [id] (unfold id' + fail)) + idtac);
+    lazymatch goal with |- id 0 = 0 => idtac end;
+    assert_fails unfold id'.
+  Fail unfold id.
+  reflexivity.
+Qed.
+
+(* test multi-success *)
+Goal id (fact 100) = fact 100.
+  Timeout 1
+          (with_strategy -1 [id] (((idtac + (abstract reflexivity))); fail)).
+  Undo.
+  Timeout 1
+          let id' := id in
+          (with_strategy -1 [id] (((idtac + (unfold id'; reflexivity))); fail)).
+  Undo.
+  Timeout 1
+          (with_strategy -1 [id] (idtac + (abstract reflexivity))); fail. (* should not time out *)
+  Undo.
+  with_strategy -1 [id] abstract reflexivity.
+Defined.
+
 (* check that module substitutions happen correctly *)
 Module F.
   Definition id {T} := @id T.