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/base.v

@@ -10,9 +10,9 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
-Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+From stdpp Require Import options.
 
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See