Commit 2023-07-14 08:37 89007158

fix: control flow errors in congr!, and add closePre and closePost for feature parity with congr (#5832) There were some accidental early returns due to adding for loops later, a missing instantiateMVars, and a max instead of a min for choosing the default iteration depth. I'm also slipping in closePre and closePost configurations to be able to turn off trying to apply rfl/Subsingleton.elim/etc., which is a feature that also exists in the core congr meta tactic.