Skip to content

Commit 0e20855

Browse files
chore(Mathlib/CategoryTheory/Sites): Deprecate CoversTop (#38810)
Follow up for #38657
1 parent 2fac168 commit 0e20855

2 files changed

Lines changed: 11 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3278,6 +3278,7 @@ public import Mathlib.CategoryTheory.Sites.CoproductSheafCondition
32783278
public import Mathlib.CategoryTheory.Sites.CoverLifting
32793279
public import Mathlib.CategoryTheory.Sites.CoverPreserving
32803280
public import Mathlib.CategoryTheory.Sites.Coverage
3281+
public import Mathlib.CategoryTheory.Sites.CoversTop
32813282
public import Mathlib.CategoryTheory.Sites.CoversTop.Basic
32823283
public import Mathlib.CategoryTheory.Sites.CoversTop.Over
32833284
public import Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
/-
2+
Copyright (c) 2023 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Sites.CoversTop.Basic
9+
10+
deprecated_module (since := "2026-05-01")

0 commit comments

Comments
 (0)