)]}'
{
  "commit": "5a8a774ce31ff91730bb3f868216cfa6297f4119",
  "tree": "06cafd51a1f0086a8d8c5b628c33e8303e29caf9",
  "parents": [
    "287d46e1f6a7a6136c7996367a9b203d93797d00"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Jun 07 12:44:18 2024 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Jun 07 12:44:18 2024 -0700"
  },
  "message": "fix: improve `split` discriminant generalization strategy\n\nThis commit also\n- improves `split` error messages.\n- adds `trace.split.failure` option.\n- uses new convention for trace messages.\n\ncloses #4390\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "fd27465d4c6ebdd6e3304342b02c9a886a7726f2",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Split.lean",
      "new_id": "0dfc669098432d1788f9f39c17e05fef28f1ed6b",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Split.lean"
    },
    {
      "type": "modify",
      "old_id": "6c625f4bd0bca6c6edc7eefb119af86582dd25aa",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Split.lean",
      "new_id": "bd20c779acfdaec63fd9fb6278660fa9afb174cf",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Split.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "4306f00ae0deff65f4529c98c3305b93874f121d",
      "new_mode": 33188,
      "new_path": "tests/lean/run/4390.lean"
    }
  ]
}