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