Library stdpp.options

Coq configuration for std++ (not meant to leak to clients). If you are a user of std++, note that importing this file means you are implicitly opting-in to every new option we will add here in the future. We are *not* guaranteeing any kind of stability here. Instead our advice is for you to have your own options file; then you can re-export the std++ file there but if we ever add an option you disagree with you can easily overwrite it in one central location.

Allow async proof-checking of sections.
#[export] Set Default Proof Using "Type".

Enforces that every tactic is executed with a single focused goal, meaning that bullets and curly braces must be used to structure the proof.
#[export] Set Default Goal Selector "!".