Start a GoodDefaults file collecting recommended option settings.

Follow-up of Zulip discussion at: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Better.20default.20options

doc/stdlib/index-list.html.template

@@ -696,13 +696,14 @@ through the <tt>Require Import</tt> command.</p>
   </dd>
 
   <dt> <b>Compat</b>:
-    Compatibility wrappers for previous versions of Coq
+    Compatibility wrappers for previous versions of Coq and recommended options at the time of a given Coq release
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
     theories/Compat/Coq818.v
     theories/Compat/Coq819.v
     theories/Compat/Coq820.v
+    theories/Compat/GoodDefaults_8_20.v
     user-contrib/Ltac2/Compat/Coq818.v
     user-contrib/Ltac2/Compat/Coq819.v
   </dd>

theories/Compat/GoodDefaults_8_20.v

@@ -0,0 +1,14 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** File exporting recommended option settings at the time of releasing Coq v8.20 *)
+
+
+#[ export ] Set Default Goal Selector "!".