From 2ec2f244c32d3d174ee0c1b8c7b1d0b32e449672 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 23 Sep 2024 17:39:31 +0200
Subject: [PATCH] clarify Smallness require

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/PropResizing/ImpredicativeTruncation.v | 2 +-
 theories/PropResizing/Nat.v                     | 2 +-
 theories/Sets/GCH.v                             | 2 +-
 theories/Sets/GCHtoAC.v                         | 2 +-
 theories/Sets/Hartogs.v                         | 2 +-
 theories/Sets/Ordinals.v                        | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/PropResizing/ImpredicativeTruncation.v b/theories/PropResizing/ImpredicativeTruncation.v
index f6fa2e8199..352a87247a 100644
--- a/theories/PropResizing/ImpredicativeTruncation.v
+++ b/theories/PropResizing/ImpredicativeTruncation.v
@@ -2,7 +2,7 @@
 (** * Impredicative truncations. *)
 
 Require Import HoTT.Basics.
-Require Import Smallness.
+Require Import Universes.Smallness.
 Local Open Scope path_scope.
 
 (* Be careful about [Import]ing this file!  It defines truncations
diff --git a/theories/PropResizing/Nat.v b/theories/PropResizing/Nat.v
index 20b57e4021..ec5bc3993b 100644
--- a/theories/PropResizing/Nat.v
+++ b/theories/PropResizing/Nat.v
@@ -3,7 +3,7 @@
 Require Import Basics.
 Require Import Types.
 Require Import HProp.
-Require Import Smallness.
+Require Import Universes.Smallness.
 Local Open Scope path_scope.
 
 (* Be careful about [Import]ing this file!  Usually you want to use the standard [Nat] instead. *)
diff --git a/theories/Sets/GCH.v b/theories/Sets/GCH.v
index 6b4a66b29f..9fd80a8d45 100644
--- a/theories/Sets/GCH.v
+++ b/theories/Sets/GCH.v
@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType abstract_algebra.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Spaces.Nat.Core Spaces.Card.
 
 Local Open Scope type.
diff --git a/theories/Sets/GCHtoAC.v b/theories/Sets/GCHtoAC.v
index 8cdae25b26..876810b3d8 100644
--- a/theories/Sets/GCHtoAC.v
+++ b/theories/Sets/GCHtoAC.v
@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType ExcludedMiddle abstract_algebra.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Spaces.Nat.Core Spaces.Card.
 From HoTT Require Import Equiv.BiInv.
 From HoTT Require Import HIT.unique_choice.
diff --git a/theories/Sets/Hartogs.v b/theories/Sets/Hartogs.v
index 755de38342..e5e8253862 100644
--- a/theories/Sets/Hartogs.v
+++ b/theories/Sets/Hartogs.v
@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Spaces.Card.
 
 From HoTT.Sets Require Import Ordinals Powers.
diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v
index d390874cbb..2f12ccdf02 100644
--- a/theories/Sets/Ordinals.v
+++ b/theories/Sets/Ordinals.v
@@ -1,5 +1,5 @@
 From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra.
-From HoTT Require Import Smallness.
+From HoTT Require Import Universes.Smallness.
 From HoTT Require Import Colimits.Quotient.
 From HoTT Require Import HSet.