Adapt test-suite to #12023.

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) ..)