fix: make `all_goals` admit goals on failure (#5934) New behavior: when in recovery mode, if any tactic fails in `all_goals` then the metacontext is restored and all goals are admitted. Without this, it can leave partially-solved metavariables and incomplete goal lists.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).