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