)]}'
{
  "commit": "b5d6940f61a81ed9257c35e2a172639282c159d1",
  "tree": "934d0c9d3b981ba0833dabbcafc8a7c5f3054ced",
  "parents": [
    "f4856ef9cd764f9eb5491b99352bf9d7d4793392"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 03:04:47 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 03:04:47 2026 +0000"
  },
  "message": "fix: respect `!` in grind\u0027s instantiate when the theorem is registered\n\nThis PR fixes `instantiate only [!thm]` ignoring the `!` modifier when `thm` is already registered as a `grind` theorem, and using its registered patterns instead of the minimal indexable ones. Generated scripts using `!thm` then failed to replay, and `grind?` dropped `thm` from its `grind only` suggestions.\n\nRegistered theorems are now reused only if they match the requested `!` modifier.\n\nCloses #16034\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "d1593601a5a5ea7810868f472a8ad2a82da5d420",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean",
      "new_id": "2931c67db70c0e379585ed07877eb50b2b6e2262",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "06b19ed044cb3e32ff1fb7a5a975895bc6e60c49",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_16034.lean"
    }
  ]
}