From fa5dccf6f3cee08994b366b0455403b85261ea3e Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 12 Sep 2023 20:09:27 -0400
Subject: [PATCH] make a few Spaces.Finite Require statements more specific

---
 theories/Algebra/Groups/Lagrange.v      | 2 +-
 theories/Algebra/Groups/QuotientGroup.v | 2 +-
 theories/Algebra/Rings/Ideal.v          | 2 +-
 theories/Analysis/Locator.v             | 2 +-
 theories/Homotopy/SuccessorStructure.v  | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Algebra/Groups/Lagrange.v b/theories/Algebra/Groups/Lagrange.v
index 050b541af73..ec20171cded 100644
--- a/theories/Algebra/Groups/Lagrange.v
+++ b/theories/Algebra/Groups/Lagrange.v
@@ -1,7 +1,7 @@
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.Subgroup.
 Require Import Algebra.Groups.QuotientGroup.
-Require Import Spaces.Finite.
+Require Import Spaces.Finite.Finite.
 Require Import Spaces.Nat.
 
 (** ** Lagrange's theorem *)
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index 48f3b40a936..88f64939d67 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -5,7 +5,7 @@ Require Export Algebra.Groups.Image.
 Require Export Algebra.Groups.Kernel.
 Require Export Colimits.Quotient.
 Require Import HSet.
-Require Import Spaces.Finite.
+Require Import Spaces.Finite.Finite.
 Require Import WildCat.
 Require Import Modalities.Modality.
 
diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 3f5bb733baa..5d46d49f327 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -1,4 +1,4 @@
-Require Import Spaces.Finite.
+Require Import Spaces.Finite.Fin.
 Require Import Algebra.Rings.CRing.
 Require Import Algebra.AbGroups.
 
diff --git a/theories/Analysis/Locator.v b/theories/Analysis/Locator.v
index dbeaa6539a2..4a59dcf04e7 100644
--- a/theories/Analysis/Locator.v
+++ b/theories/Analysis/Locator.v
@@ -2,7 +2,7 @@ Require Import
         HoTT.Basics
         HoTT.DProp
         HoTT.BoundedSearch
-        HoTT.Spaces.Finite
+        HoTT.Spaces.Finite.Fin
         HoTT.ExcludedMiddle.
 
 Require Import
diff --git a/theories/Homotopy/SuccessorStructure.v b/theories/Homotopy/SuccessorStructure.v
index de70b758ccb..a908e93f3be 100644
--- a/theories/Homotopy/SuccessorStructure.v
+++ b/theories/Homotopy/SuccessorStructure.v
@@ -1,6 +1,6 @@
 Require Import Basics.
 Require Import Spaces.Int.
-Require Import Spaces.Finite.
+Require Import Spaces.Finite.Fin.
 
 (** * Successor Structures. *)