commit: b31003bf2580423f47feea7c0d4181a5ba21bbd4

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Sat Dec 14 15:37:54 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Dec 14 16:25:13 2024 -0800
tree: ca7609304b120c299e6f6af11a21c31a6a91939b
parent: b721c0f54041f6a6adc618c07851a7e0414bd1e4 [diff]

fix: `revertAll` must clear auxiliary declarations

This PR ensures that `revertAll` clears auxiliary declarations when
invoked directly by users.

closes #6263

src/Lean/Meta/Tactic/Grind/RevertAll.lean[diff]
tests/lean/run/6263.lean[Added - diff]

2 files changed

tree: ca7609304b120c299e6f6af11a21c31a6a91939b

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).