diff options
| author | Anton Trunov | 2020-05-15 11:35:09 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-05-15 11:35:09 +0300 |
| commit | 959254ccd5c895782286dfb1d2c731e143e37d00 (patch) | |
| tree | 338b029fc34d3a9abb53ad011374986e9e894832 | |
| parent | a605c48898b29a66fc623493afdb73650026c2a6 (diff) | |
| parent | 7510aa6d49cbc48962ee29949b61f1bed2b27e1a (diff) | |
Merge PR #11992: do not re-export ListNotations from Program
Reviewed-by: Zimmi48
Reviewed-by: anton-trunov
Reviewed-by: ejgallego
| -rw-r--r-- | doc/changelog/10-standard-library/11992-no-reexports.rst | 4 | ||||
| -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 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 3 |
5 files changed, 7 insertions, 5 deletions
diff --git a/doc/changelog/10-standard-library/11992-no-reexports.rst b/doc/changelog/10-standard-library/11992-no-reexports.rst new file mode 100644 index 0000000000..3f46bfd501 --- /dev/null +++ b/doc/changelog/10-standard-library/11992-no-reexports.rst @@ -0,0 +1,4 @@ +- **Changed:** + No longer re-export ``ListNotations`` from ``Program`` (``Program.Syntax``) + (`#11992 <https://github.com/coq/coq/pull/11992>`_, + by Antonio Nikishaev). 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. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 03401aea2b..7a8ddbe71e 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -30,7 +30,4 @@ Arguments snd {A B} _. Arguments nil {A}. Arguments cons {A} _ _. -Require List. -Export List.ListNotations. - Require Import Bvector. |