)]}'
{
  "commit": "589c4ba3eabef4f82e9ee89bb922dc97b7972894",
  "tree": "db3474fe0db37dc2d0478413bf1128095a4c3498",
  "parents": [
    "85b462f23c73be9493e258db7d86fc941fa0f815"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 04:28:13 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 04:28:13 2026 +0000"
  },
  "message": "fix: keep case-splits needed to replay `grind?` scripts\n\nThis PR fixes `grind?` and `finish?` dropping case-splits from their generated scripts when the proof does not use the case-split, but the rest of the script does. For example, a case-split may introduce a term that E-matching uses later. The scripts then failed to replay, and `grind?` dropped theorems from its `grind only` suggestions.\n\nWhen generating a script, non-chronological backtracking now drops a case-split only if the script still closes the goal without it. Otherwise, the case-split is kept and its remaining alternatives are explored. If they cannot be closed, the case-split is dropped as before.\n\nCloses #16037\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c664e42acb08c8f6cb31409bf7e79e13f8401e9d",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Split.lean",
      "new_id": "94153cdab4dcff9592710f7b7b73f1797a4bb0a2",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Split.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "1cad01b7f1dbe6e1029c77a959f79fa0061c5cc1",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_16037.lean"
    }
  ]
}