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 /test-suite | |
| 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
Diffstat (limited to 'test-suite')
| -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. |