feat: make sure `clear_value` preserves local context order (#8792)

This PR makes the `clear_value` tactic preserve the order of variables
in the local context. This is done by adding
`Lean.MVarId.withRevertedFrom`, which reverts all local variables
starting from a given variable, rather than only the ones that depend on
it.

Note: an alternative implementation might convert the ldecl to a cdecl
and then reset the meta cache. This assumes that there are no other
caches that might still remember the value of the ldecl.
3 files changed