)]}'
{
  "commit": "764dca121680e2ad8db274f96bf117c369af9abf",
  "tree": "4f0d9e2ba202ff3fc4dabe91be37f367afb24d78",
  "parents": [
    "b8a13ab755317e4af3a4a99bd92fae26aa6a75b2"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Nov 17 17:52:19 2024 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Nov 17 17:58:33 2024 -0800"
  },
  "message": "fix: backtrack at `injection` failure\n\nThis PR fixes an issue in the `injection` tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment.\nThis issue was causing the error: \"`mvarId` is already assigned\" in issue #6066.\nThe issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "09250f73388bda7bfd08a06ac61b5c77ba567f11",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Injection.lean",
      "new_id": "f45ccee1696d013175e02afd2c0b1f1a9c845d30",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Injection.lean"
    }
  ]
}