Library stdpp.options

Iris sets some Rocq flags for itself that we do not want to impose on downstream clients by default. Those flags are configured in config/flags so they are set as command-line parameters in our Rocq invocations. This file exists as an old deprecated way to achieve the same effect: Importing this file sets these flags without leaking them to downstream clients. Please do not import this file into new projects; instead, copy-paste the -set flags from config/flags into your _RocqProject (with -arg).

Allow async proof-checking of sections.

Enforces that every tactic is executed with a single focused goal, meaning that bullets and curly braces must be used to structure the proof.