do not re-export ListNotations from Program: fix testsuite

coq · Apr 30, 2020 · 4a47406 · 4a47406
1 parent 1175ca0
commit 4a47406
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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.