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