Add "options" file

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. :)

Thanks and LGTM modulo nits.

added 1 commit

• 5f61cb23 - fix base.v import order

Compare with previous version

added 1 commit

• 92aceef1 - fix base.v import order; use real import in prelude.v

Compare with previous version

resolved all threads

mentioned in commit 233bed09

merged