Add "options" file like in Iris
@robbertkrebbers would you like me to add an "options" file here like in Iris? Only parts of std++ use Set Default Proof using
, but we could make that opt-out instead of opt-in. We could also do iris#344 (closed) in std++.
I can add the basic options file and the check to make sure it is imported everywhere, but I am not sure if I will have the time to also adjust everything to work with Default Proof Using
or Goal Selector
.