From 9eca531a874dc8f71cf21c708044c1cd11a6c1f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Thu, 30 May 2024 15:48:24 +0200
Subject: [PATCH] Start a GoodDefaults file collecting recommended option
 settings.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Théo Winterhalter <theo.winterhalter@inria.fr>

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

Co-authored-by: Théo Zimmermann <theo.zimmermann@telecom-paris.fr>
---
 .../11-corelib/19117-good-defaults-Added.rst  |  5 +++
 doc/corelib/index-list.html.template          |  2 +
 doc/sphinx/language/core/basic.rst            | 14 +++++++
 theories/Corelib/Compat/GoodDefaults_2025.v   | 42 +++++++++++++++++++
 4 files changed, 63 insertions(+)
 create mode 100644 doc/changelog/11-corelib/19117-good-defaults-Added.rst
 create mode 100644 theories/Corelib/Compat/GoodDefaults_2025.v

diff --git a/doc/changelog/11-corelib/19117-good-defaults-Added.rst b/doc/changelog/11-corelib/19117-good-defaults-Added.rst
new file mode 100644
index 000000000000..4d4a31b005b9
--- /dev/null
+++ b/doc/changelog/11-corelib/19117-good-defaults-Added.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  A GoodDefaults_2025 module setting various options to their recommended value,
+  see :ref:`the doc <good_defaults>` for more details
+  (`#19117 <https://github.com/rocq-prover/rocq/pull/19117>`_,
+  by Théo Zimmermann and Théo Winterhalter).
diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template
index 11472171ef39..613a64308866 100644
--- a/doc/corelib/index-list.html.template
+++ b/doc/corelib/index-list.html.template
@@ -163,6 +163,7 @@ through the <tt>Require Import</tt> command.</p>
 
   <dt id="Compat"> <a href="#Compat"><b>Compat</b></a>:
     Compatibility wrappers for previous versions of Coq
+     and recommended options at the time of a given Rocq release
   </dt>
   <dd>
     theories/Corelib/Compat/Coq818.v
@@ -170,6 +171,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Corelib/Compat/Coq820.v
     theories/Corelib/Compat/Rocq90.v
     theories/Corelib/Compat/Rocq91.v
+    theories/Corelib/Compat/GoodDefaults_2025.v
     theories/Ltac2/Compat/Coq818.v
     theories/Ltac2/Compat/Coq819.v
   </dd>
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 5bbc3d3839fd..05dcc3df53f2 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -400,6 +400,20 @@ The :term:`flag`, :term:`option` and :term:`table`
 mechanisms are used to modify the behavior of Rocq more globally in a
 document or project.
 
+.. _good_defaults:
+
+The default value of some settings is not the one that would be recommended
+today for compatibility reasons. We provide a *good default* file in the Corelib
+which can be imported as follows:
+
+.. rocqtop:: in
+
+   From Corelib Require Import GoodDefaults_2025.
+
+This file is versioned to account for the changes in recommendations as the Rocq
+practice evolves. The 2025 edition will remain available without change after
+future versions are released.
+
 .. _attributes:
 
 Attributes
diff --git a/theories/Corelib/Compat/GoodDefaults_2025.v b/theories/Corelib/Compat/GoodDefaults_2025.v
new file mode 100644
index 000000000000..b5cd54b4c94a
--- /dev/null
+++ b/theories/Corelib/Compat/GoodDefaults_2025.v
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** * Good defaults 2025
+
+  File exporting recommended option settings at the time of releasing Rocq v9.1
+
+*)
+
+#[ export ] Set Default Goal Selector "!".
+
+#[ export ] Set Asymmetric Patterns.
+
+#[ export ] Set Keyed Unification.
+
+(** The following affect people using [Universe Polymorphism]. *)
+
+#[ export ] Set Polymorphic Inductive Cumulativity.
+
+#[ export ] Set Typeclasses Default Mode "!".
+Hint Constants Opaque : typeclass_instances.
+
+Ltac Tauto.intuition_solver ::= auto with core.
+
+(** Makes the behavior of [injection] consistent with the rest of standard
+  tactics.
+*)
+
+#[ export ] Set Structural Injection.
+
+(** These three affect pepole that set [Implicit Arguments]. *)
+
+#[ export ] Set Strongly Strict Implicit.
+#[ export ] Set Maximal Implicit Insertion.
+#[ export ] Set Contextual Implicit.