Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace -type-in-type by #[local] Unset Universe Checking in all necessary files #1698

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Replace -type-in-type by #[local] Unset Universe Checking in all necessary files #1698

Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
8b8a3d6
Replaced “-type-in-type” with “Unset Universe Checking”
peterlefanulumsdaine May 22, 2023
054293c
changed deprecated ‘Export Unset’ to ‘#[export] Unset’
peterlefanulumsdaine May 23, 2023
92e5157
Completed localizing ‘Unset Universe Checking’ within Foundations pac…
peterlefanulumsdaine May 23, 2023
b251083
Completed localizing ‘Unset Universe Checking’ within MoreFoundations…
peterlefanulumsdaine May 23, 2023
4360341
Localised ‘Unset Universe Checking’ per file in all packages up tp PA…
peterlefanulumsdaine May 23, 2023
c64dd30
Localised ‘Unset Universe Checking’ per file in most packages up to
peterlefanulumsdaine May 23, 2023
2d938ee
Localised ‘Unset Universe Checking’ per file in all packages except C…
peterlefanulumsdaine May 23, 2023
1eae604
Localised ‘Unset Universe Checking’ per file in CategoryTheory
peterlefanulumsdaine May 23, 2023
b4a04e4
Localised ‘Unset Universe Checking’ per file in HomologicalAlgebra
peterlefanulumsdaine May 23, 2023
e3b8328
Localised ‘Unset Universe Checking’ per file in Bicategories (complet…
peterlefanulumsdaine May 23, 2023
9a7bf29
Removed a couple of erroneous duplicate Unsets
peterlefanulumsdaine May 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Localised ‘Unset Universe Checking’ per file in HomologicalAlgebra
  • Loading branch information
@peterlefanulumsdaine
peterlefanulumsdaine committed May 23, 2023
commit b4a04e4236d4bd9dda7495b25d4aabe860cb8c5d
1 change: 1 addition & 0 deletions UniMath/HomologicalAlgebra/Complexes.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
#[local] Unset Universe Checking.
(** * The category of complexes over an additive category *)
(** ** Contents
- Definition of complexes [def_complexes]
Expand Down