Skip to content

Add "options" file

Ralf Jung requested to merge ralf/options into master

Fixes #81 (closed)

There is a slight chance that setting Set Default Proof Using "Type*" in a file where the option was not present before adds some extra assumptions to lemmas. I made sure everything still compiles and will also test Iris against this branch. But @robbertkrebbers if you want to be extra sure this doesn't add any unnecessary assumptions elsewhere, I will make those files Unset Default Proof Using; someone will have to manually investigate each lemma to check the assumptions.

Thanks to @tchajed we can even set the default goal selector. :)

Merge request reports