Commit 2026-01-29 13:31 6a39ceeb

feat(Tactic/ApplyWith): use a config_elab for apply (config := cfg) (#34524) This PR replaces the custom syntax for apply (config := cfg) with the standard optConfig and declare_config_elab. This means we can now write apply +allowSynthFailures instead of apply (config := { allowSynthFailures := true }). Also redo the tactic doc so it is alternative of the plain apply tactic, rather than having it have own documentation.