`revert` does not respect the argument order

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The revert tactic ignores the order of its arguments

Context

[Broader context that the issue occured in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

example (a b c : Nat) : a * b * c = 1 := by
  revert c a b
  sorry

Expected behavior: Goal is ∀ (c a b : Nat), a * b * c = 1 like it was in Lean 3

Actual behavior: Goal is ∀ (a b c : Nat), a * b * c = 1, ignoring the argument order

Versions

4.4.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal revert c a b example in the issue and compare the produced goal with the expected order. Locate the Lean 4 revert tactic implementation, then add a regression test showing that argument order is preserved and run the relevant tactic tests.