)]}'
{
  "commit": "f46005fe573ec92abf9d70c57eb5c7d5cff0dd33",
  "tree": "79884464ece77ac57ad2034d007a68a9b20f3d0c",
  "parents": [
    "bda15f6c25557f2b9e4062e640562fc9370e3069"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sun Feb 15 14:36:35 2026 +1100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Feb 16 08:47:07 2026 +1100"
  },
  "message": "perf: skip `preprocessOutParam` for noMVars queries\n\nThis reverts part of the `OrderDual` workaround from #12286.\n\nThe `preprocessOutParam` step is morally not needed when the type has\nno metavariables, because output params should be uniquely determined\nby the input params. The optimization was removed because\nsemireducible type aliases like `OrderDual` caused TC resolution to\nfail (e.g. `FunLike F (OrderDual α) (OrderDual β)` where the last\ntwo arguments are output parameters — without `preprocessOutParam`,\nTC resolution fails because it cannot unfold `OrderDual`).\n\nThis is an experimental branch for testing whether Mathlib\u0027s\n`OrderDual` refactoring has progressed enough to restore this\noptimization.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "43d828e069af49ab78881fe4d3c3adadf641c944",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/SynthInstance.lean",
      "new_id": "e5954907b96b477644d09bd0114ff2a3b1fa3beb",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/SynthInstance.lean"
    }
  ]
}