Merge pull request #1757 from jdchristensen/require-finite-specific

make a few Spaces.Finite Require statements more specific
HoTT · Sep 13, 2023 · c56c27b · c56c27b
2 parents 6486ff3 + fa5dccf
commit c56c27b
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1,6 +1,6 @@
 Require Import Basics.
 Require Import Spaces.Int.
-Require Import Spaces.Finite.
+Require Import Spaces.Finite.Fin.
 
 (** * Successor Structures. *)