Skip to content

Make stdpp compatible with Set Default Proof Selector "!"

Set Default Goal Selector "!" makes it illegal to ever apply a tactic with more than one goal (instead, must focus with bullets or braces). Currently std++ violates this all over the place, particularly with split followed by two short proofs.

Turning on the option relies on #81 (closed).

Edited by Tej Chajed