Merge PR #12023: Adding a Declare ML Module in empty file Ltac.v

Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot

22 files changed, 64 insertions, 10 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
new file mode 100644
index 0000000000..6bee3c7bb6
--- /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+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
+
+    mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+    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+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    unimath_CI_GITURL=https://github.com/herbelin/UniMath
+
+fi
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).
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/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) ..)
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/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..da540cb099 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -129,9 +129,3 @@ Bind Scope type_scope with Sortclass.
 Open Scope core_scope.
 Open Scope function_scope.
 Open Scope type_scope.
-
-(** ML Tactic Notations *)
-
-Declare ML Module "ltac_plugin".
-
-Global Set Default Proof Mode "Classic".
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.
 
diff --git a/theories/ltac/Ltac.v b/theories/ltac/Ltac.v
deleted file mode 100644
index e69de29bb2..0000000000
--- a/theories/ltac/Ltac.v
+++ /dev/null