Skip to content

Alternative definition of `no_new_unsolved_evars` tactic

Robbert Krebbers requested to merge robbert/no_new_unsolved_evars into master

Following a suggestion by @jung in !429 (diffs, comment 86725)

@jung Could you run CI on all reverse dependencies to see if this indeed does not break anything?

Todo:

  • Also improve naming to make sure this tactic either solves or fails.

Merge request reports