diff options
| author | Jason Gross | 2020-05-09 14:02:46 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 14:04:42 -0400 |
| commit | 6e4ebb2dbaa2cb9eb70ce205386bee08c80aaa00 (patch) | |
| tree | f4c5ce1ff2aeee5e3a7b60598fdd0b9b276f941f | |
| parent | 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd (diff) | |
Add another note about removing a tactic after abstract
| -rw-r--r-- | tactics/tactics.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c1b1076102..c2654486e1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5090,11 +5090,11 @@ 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 *) + (* 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 + let orig_kl_global = ... in *) let orig_kl_global = List.map (fun (_lvl, k) -> (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k)) kl in @@ -5102,6 +5102,8 @@ let with_set_strategy lvl_ql 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, remove this + [Proofview.tclLIFT] block *) Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*> Proofview.tclUNIT (orig_kl, orig_kl_global)) |