Fix the `with_strategy` tactic to work with `abstract`

3 files changed, 29 insertions, 6 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fd6b2b3846..b376d9177f 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3370,7 +3370,9 @@ the conversion in hypotheses :n:`{+ @ident}`.
       Use this tactic with care, as effects do not persist past the
       end of the proof script.  Notably, this fine-tuning of the
       conversion strategy is not in effect during :cmd:`Qed` nor
-      :cmd:`Defined`, so this tactic is most useful to guard
+      :cmd:`Defined`, so this tactic is most useful either in
+      combination with :tacn:`abstract`, which will check the proof
+      early while the fine-tuning is still in effect, or to guard
       calls to conversion in tactic automation to ensure that, e.g.,
       :tacn:`unfold` does not fail just because the user made a
       constant :cmd:`Opaque`.
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b17f02f224..350881f72d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5057,16 +5057,37 @@ let with_set_strategy lvl_ql k =
   let orig_kl = List.map (fun (_lvl, k) ->
       (Conv_oracle.get_strategy (Environ.oracle env) k, k))
       kl in
+  (* Because the global env might be desynchronized from the proof-local
+     env, we need to update the global env to have this tactic play
+     nicely with abstract.
+     TODO: When abstract no longer depends on Global, delete this variable
+       let-in *)
+  let orig_kl_global = List.map (fun (_lvl, k) ->
+      (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k))
+      kl in
   let env = List.fold_left (fun env (lvl, k) ->
     Environ.set_oracle env
       (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
-  Proofview.Unsafe.tclSETENV env <*>
+  (* TODO: When abstract no longer depends on Global, replace this
+       [Proofview.Goal.enter] block with [Proofview.Unsafe.tclSETENV env] *)
+  Proofview.Goal.enter begin
+    fun _ ->
+      List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl;
+      Proofview.Unsafe.tclSETENV env
+  end <*>
   k <*>
   Proofview.tclENV >>= fun env ->
   let env = List.fold_left (fun env (lvl, k) ->
-    Environ.set_oracle env
-      (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
-  Proofview.Unsafe.tclSETENV env
+      Environ.set_oracle env
+        (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
+  Proofview.Unsafe.tclSETENV env <*>
+  (* TODO: When abstract no longer depends on Global, remove this
+       [Proofview.Goal.enter] block *)
+  Proofview.Goal.enter begin
+    fun _ ->
+      List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global;
+      Proofview.tclUNIT ()
+  end
 
 module Simple = struct
   (** Simplified version of some of the above tactics *)
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index bf639ae6b9..bacea3549f 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -131,7 +131,7 @@ Qed.
 (* test that the strategy tactic does persist through abstract *)
 Opaque id.
 Goal id 0 = 0.
-  Fail Time Timeout 5
+  Time Timeout 5
        with_strategy
        expand [id]
        assert (id (fact 100) = fact 100) by abstract reflexivity.