Commit 2023-02-11 15:01 f00c9564

feat: port Tactic.Group (#2122) We implement group by alternating between a simp call and ring_nf (to normalize the exponents) until no progress is made. To do this we also implement the tactic fail_if_no_progress, so that repeat (fail_if_no_progress (simp ... <;> ring_nf)) behaves as expected.