This provides an easy way for us to set some Coq options in every file in Iris, without affecting user developments. For now we just do
Set Default Proof Using "Type".
but once we have this infrastructure, there might be more things we want to use it for.
This is not yet added to all files as I wanted to first solicit feedback. The following command prints the files that forget to import the options file:
for FILE in $(find theories/ -name "*.v" | fgrep -v theories/options.v); do if ! fgrep -q 'From iris Require Import options.' "$FILE"; then echo "$FILE"; fi done
We should probably check this to be empty on CI.
Fixes #66 (closed).