From c6815a6cd004a1ab4852414127fef6f8f77894bb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Apr 2020 14:13:54 +0200
Subject: Adding a Declare ML Module in empty file Ltac.v.

Indeed, it would be intuitive that `Require Import Ltac` is an
equivalent for Ltac of `Require Import Ltac2.Ltac2`.

Also declaring the classic proof mode.
---
 .../12023-herbelin-master+fixing-empty-Ltac-v-file.sh     | 15 +++++++++++++++
 doc/stdlib/index-list.html.template                       |  1 +
 theories/Init/Ltac.v                                      | 13 +++++++++++++
 theories/Init/Notations.v                                 |  4 +---
 theories/ltac/Ltac.v                                      |  0
 5 files changed, 30 insertions(+), 3 deletions(-)
 create mode 100644 dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
 create mode 100644 theories/Init/Ltac.v
 delete mode 100644 theories/ltac/Ltac.v

diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
new file mode 100644
index 0000000000..e2c27c939e
--- /dev/null
+++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
+
+    fiat_crypto_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
+
+    mtac2_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+    metacoq_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    metacoq_CI_GITURL=https://github.com/herbelin/template-coq
+
+    unimath_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    unimath_CI_GITURL=https://github.com/herbelin/UniMath
+
+fi
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7fa621c11c..b181951767 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -13,6 +13,7 @@ through the <tt>Require Import</tt> command.</p>
     The core library (automatically loaded when starting Coq)
   </dt>
   <dd>
+    theories/Init/Ltac.v
     theories/Init/Notations.v
     theories/Init/Datatypes.v
     theories/Init/Logic.v
diff --git a/theories/Init/Ltac.v b/theories/Init/Ltac.v
new file mode 100644
index 0000000000..ac5a69a38a
--- /dev/null
+++ b/theories/Init/Ltac.v
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+Declare ML Module "ltac_plugin".
+
+Export Set Default Proof Mode "Classic".
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index a5e4178b93..833fb7464e 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -132,6 +132,4 @@ Open Scope type_scope.
 
 (** ML Tactic Notations *)
 
-Declare ML Module "ltac_plugin".
-
-Global Set Default Proof Mode "Classic".
+Require Export Ltac.
diff --git a/theories/ltac/Ltac.v b/theories/ltac/Ltac.v
deleted file mode 100644
index e69de29bb2..0000000000
-- 
cgit v1.2.3


From 94b2c08221b950232d43e6e4273afc70c75318e4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 10:42:53 +0200
Subject: Moving the main Require Export Ltac in Prelude.v.

---
 theories/Init/Byte.v       |  1 +
 theories/Init/Datatypes.v  |  1 +
 theories/Init/Logic.v      |  1 +
 theories/Init/Logic_Type.v |  1 +
 theories/Init/Notations.v  |  4 ----
 theories/Init/Peano.v      |  1 +
 theories/Init/Prelude.v    |  3 ++-
 theories/Init/Specif.v     |  1 +
 theories/Init/Tactics.v    |  1 +
 theories/Init/Tauto.v      | 13 +++++++++++++
 theories/Init/Wf.v         |  1 +
 11 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v
index 33eabb20d9..7449b52d76 100644
--- a/theories/Init/Byte.v
+++ b/theories/Init/Byte.v
@@ -10,6 +10,7 @@
 
 (** * Bytes *)
 
+Require Import Coq.Init.Ltac.
 Require Import Coq.Init.Datatypes.
 Require Import Coq.Init.Logic.
 Require Import Coq.Init.Specif.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 50d4314a6b..0f2717beef 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -11,6 +11,7 @@
 Set Implicit Arguments.
 
 Require Import Notations.
+Require Import Ltac.
 Require Import Logic.
 
 (********************************************************************)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ae48febc49..8f9f68a292 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -11,6 +11,7 @@
 Set Implicit Arguments.
 
 Require Export Notations.
+Require Import Ltac.
 
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
 
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index d07fe68715..3d9937ae89 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -13,6 +13,7 @@
 
 Set Implicit Arguments.
 
+Require Import Ltac.
 Require Import Datatypes.
 Require Export Logic.
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 833fb7464e..da540cb099 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -129,7 +129,3 @@ Bind Scope type_scope with Sortclass.
 Open Scope core_scope.
 Open Scope function_scope.
 Open Scope type_scope.
-
-(** ML Tactic Notations *)
-
-Require Export Ltac.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 394fa879c4..02903643d4 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -26,6 +26,7 @@
  *)
 
 Require Import Notations.
+Require Import Ltac.
 Require Import Datatypes.
 Require Import Logic.
 Require Coq.Init.Nat.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 71ba3e645d..6a81517d7e 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -18,10 +18,11 @@ Require Coq.Init.Decimal.
 Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
+Require Export Coq.Init.Ltac.
 Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
 (* Some initially available plugins. See also:
-   - ltac_plugin (in Notations)
+   - ltac_plugin (in Ltac)
    - tauto_plugin (in Tauto).
 *)
 Declare ML Module "cc_plugin".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 59ee252d35..4ff007570e 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -14,6 +14,7 @@ Set Implicit Arguments.
 Set Reversible Pattern Implicit.
 
 Require Import Notations.
+Require Import Ltac.
 Require Import Datatypes.
 Require Import Logic.
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index a4347bbe62..b13206db94 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import Notations.
+Require Import Ltac.
 Require Import Logic.
 Require Import Specif.
 
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 87b7a9a3be..2fc6f3cfa6 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -1,4 +1,17 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** * The tauto and intuition tactics *)
+
 Require Import Notations.
+Require Import Ltac.
 Require Import Datatypes.
 Require Import Logic.
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 06afd9bac0..a305626eb3 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -16,6 +16,7 @@
 Set Implicit Arguments.
 
 Require Import Notations.
+Require Import Ltac.
 Require Import Logic.
 Require Import Datatypes.
 
-- 
cgit v1.2.3


From cc0aa0d6e9a8fafbd42c90cdfda8e9be590c03cb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Apr 2020 13:47:53 +0200
Subject: Adapt test-suite to #12023.

---
 test-suite/bugs/closed/HoTT_coq_107.v | 1 +
 test-suite/bugs/closed/bug_3881.v     | 1 +
 test-suite/bugs/closed/bug_4527.v     | 2 +-
 test-suite/bugs/closed/bug_4533.v     | 2 +-
 test-suite/bugs/closed/bug_4544.v     | 2 +-
 test-suite/bugs/closed/bug_6661.v     | 1 +
 6 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
index fa4072a8f6..91f5c423a5 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
 (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
 Require Import Coq.Init.Logic.
+Require Import Coq.Init.Ltac.
 Global Set Universe Polymorphism.
 Global Set Asymmetric Patterns.
 Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/bug_3881.v b/test-suite/bugs/closed/bug_3881.v
index d7e097e326..50e9de60e5 100644
--- a/test-suite/bugs/closed/bug_3881.v
+++ b/test-suite/bugs/closed/bug_3881.v
@@ -4,6 +4,7 @@
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
 Generalizable All Variables.
 Require Import Coq.Init.Notations.
+Require Import Coq.Init.Ltac.
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Axiom admit : forall {T}, T.
diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v
index dfb07520f1..cf802eb89b 100644
--- a/test-suite/bugs/closed/bug_4527.v
+++ b/test-suite/bugs/closed/bug_4527.v
@@ -5,7 +5,7 @@ then from 269 lines to 255 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml
 4.01.0
    coqtop version 8.5 (January 2016) *)
-Declare ML Module "ltac_plugin".
+Require Import Coq.Init.Ltac.
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/bug_4533.v b/test-suite/bugs/closed/bug_4533.v
index d2f9fb9099..2d628f414d 100644
--- a/test-suite/bugs/closed/bug_4533.v
+++ b/test-suite/bugs/closed/bug_4533.v
@@ -5,7 +5,7 @@ then from 285 lines to 271 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml
 4.01.0
    coqtop version 8.5 (January 2016) *)
-Declare ML Module "ltac_plugin".
+Require Import Coq.Init.Ltac.
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v
index e9e9c552f6..213c91bfa0 100644
--- a/test-suite/bugs/closed/bug_4544.v
+++ b/test-suite/bugs/closed/bug_4544.v
@@ -2,7 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
    coqtop version 8.5 (January 2016) *)
-Declare ML Module "ltac_plugin".
+Require Import Coq.Init.Ltac.
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v
index 28a9ffc7bd..0f4ae2b4c5 100644
--- a/test-suite/bugs/closed/bug_6661.v
+++ b/test-suite/bugs/closed/bug_6661.v
@@ -7,6 +7,7 @@
 
 
 Require Export Coq.Init.Notations.
+Require Export Coq.Init.Ltac.
 Notation "'∏'  x .. y , P" := (forall x, .. (forall y, P) ..)
   (at level 200, x binder, y binder, right associativity) : type_scope.
 Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
-- 
cgit v1.2.3


From 7f4092718deed6c3d492ef3a1be16cef51212c14 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 18 Apr 2020 14:50:01 +0200
Subject: Overlay for fiat-crypto, Mtac2, MetaCoq and UniMath.

---
 .../12023-herbelin-master+fixing-empty-Ltac-v-file.sh             | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
index e2c27c939e..6bee3c7bb6 100644
--- a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
+++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
@@ -1,15 +1,15 @@
 if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
 
-    fiat_crypto_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
     fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
 
-    mtac2_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
     mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
 
-    metacoq_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
     metacoq_CI_GITURL=https://github.com/herbelin/template-coq
 
-    unimath_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file
+    unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
     unimath_CI_GITURL=https://github.com/herbelin/UniMath
 
 fi
-- 
cgit v1.2.3


From 9664a490ac3755b19ed9b8ec6a2f1925d9ec79ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 16:42:54 +0200
Subject: Change log for #12023

Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
---
 doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst

diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst
new file mode 100644
index 0000000000..f10208e9b2
--- /dev/null
+++ b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Tactics with qualified name of the form ``Coq.Init.Notations`` are
+  now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit
+  option should now import Coq.Init.Ltac if they want to use Ltac
+  (`#12023 <https://github.com/coq/coq/pull/12023>`_,
+  by Hugo Herbelin; minor source of incompatibilities).
-- 
cgit v1.2.3