)]}'
{
  "commit": "890e115000dbccbac4251834b67578047a4d6e6c",
  "tree": "ba1f947e10652ce0b80945930afd5fe1821c6b50",
  "parents": [
    "7376eb82afe9005f2e6e04aca3cc7b097e9d69a4"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 02:44:33 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 03:46:55 2026 +0000"
  },
  "message": "fix: do not generate `· done` for alternatives closed by `cases` in grind scripts\n\nThis PR fixes `grind?` generating a `· done` step for a case-split alternative that `grind` closes while introducing its hypotheses. The step failed when the script was replayed, which also made `grind?` drop theorems from its `grind only` suggestions.\n\n`Action.group` now keeps an empty tactic sequence empty instead of turning it into `· done`, matching how `splitCore` treats such alternatives.\n\nCloses #16032\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "15c4d03de77d77d634354211c68eac7f17e7db2b",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Action.lean",
      "new_id": "a0610bfa73f13b4234c9552613fe2badd9dca17d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Action.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "49831d3a02f9fb6b2337c228c1db1bd7e0708017",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_16032.lean"
    }
  ]
}