diff options
| author | Antonio Nikishaev | 2020-04-30 00:45:34 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-30 13:26:00 +0400 |
| commit | 4a474065cdd12591cf3a45358b0bd446834b2670 (patch) | |
| tree | 33c2972c9d1e7bcdd7532e7a2a7c1e576719858e | |
| parent | 1175ca0573cb13bf59148ebdab347a62875ad95e (diff) | |
do not re-export ListNotations from Program: fix testsuite
| -rw-r--r-- | test-suite/bugs/closed/bug_2830.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4151.v | 2 | ||||
| -rw-r--r-- | 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 a321bb324e..16ba02b340 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 9ec8c01ac6..df3c9481a6 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 18ebcd6384..ce07512a1e 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. |