From 33388d18f0165369a565cd5ca5b6eb153899271e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 19 Apr 2020 18:04:14 -0400
Subject: Fix the `with_strategy` tactic to work with `abstract`

---
 tactics/tactics.ml | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

(limited to 'tactics')

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 *)
-- 
cgit v1.2.3