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

theories/options.v

@@ -4,6 +4,9 @@ file is *imported*, the option will only apply on the import site
 but not transitively. *)
 
 Export Set Default Proof Using "Type".
+(* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
+Export Set Suggest Proof Using. *)
+Export Set Default Goal Selector "!".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.