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

1 files changed, 25 insertions, 4 deletions

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 *)