From 4a474065cdd12591cf3a45358b0bd446834b2670 Mon Sep 17 00:00:00 2001
From: Antonio Nikishaev <me@lelf.lu>
Date: Thu, 30 Apr 2020 00:45:34 +0400
Subject: [PATCH] do not re-export ListNotations from Program: fix testsuite

---
 test-suite/bugs/closed/bug_2830.v | 2 +-
 test-suite/bugs/closed/bug_4151.v | 2 +-
 test-suite/success/Record.v       | 1 +
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v
index a321bb324ee6..16ba02b3409f 100644
--- a/test-suite/bugs/closed/bug_2830.v
+++ b/test-suite/bugs/closed/bug_2830.v
@@ -208,7 +208,7 @@ Defined.
 
 (* The [list] type constructor is a Functor. *)
 
-Import List.
+Require Import List.
 
 Definition setList (A:set_cat) := list A.
 Instance list_functor : Functor set_cat set_cat setList.
diff --git a/test-suite/bugs/closed/bug_4151.v b/test-suite/bugs/closed/bug_4151.v
index 9ec8c01ac6b8..df3c9481a6ec 100644
--- a/test-suite/bugs/closed/bug_4151.v
+++ b/test-suite/bugs/closed/bug_4151.v
@@ -9,7 +9,7 @@ Qed.
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
 Require Import Coq.Lists.SetoidList.
-Require Export Coq.Program.Program.
+Import ListNotations.
 
 Global Set Implicit Arguments.
 Global Set Asymmetric Patterns.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 18ebcd63844e..ce07512a1efb 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -3,6 +3,7 @@ Definition CProp := Prop.
 Record test : CProp :=  {n : nat ; m : bool ; _ : n <> 0 }.
 Require Import Program.
 Require Import List.
+Import ListNotations.
 
 Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
 Arguments vector : clear implicits.