diff --git a/theories/base.v b/theories/base.v
index 933535d5ca4389a807d715909d2f763f8d703be6..6f02d571db28f866a8a251f4caa11f742cea015e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1125,13 +1125,6 @@ Class FreshSpec A C `{ElemOf A C,
   is_fresh (X : C) : fresh X ∉ X
 }.
 
-(** The class [Infinite] axiomatizes types with infinitely many elements
-by giving an injection from the natural numbers into the type. It is mostly
-used to provide a generic [fresh] algorithm. *)
-Class Infinite A :=
-  { inject: nat → A;
-    inject_injective:> Inj (=) (=) inject }.
-
 (** * Miscellaneous *)
 Class Half A := half: A → A.
 Hint Mode Half ! : typeclass_instances.
diff --git a/theories/infinite.v b/theories/infinite.v
index 79739fbc40e151c0db5a804559f79c08b6052dbf..dba8a0b91ccb6d977d8c832f8a77d7367d945148 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -2,6 +2,13 @@
 (* This file is distributed under the terms of the BSD license. *)
 From stdpp Require Import pretty fin_collections.
 
+(** The class [Infinite] axiomatizes types with infinitely many elements
+by giving an injection from the natural numbers into the type. It is mostly
+used to provide a generic [fresh] algorithm. *)
+Class Infinite A :=
+  { inject: nat → A;
+    inject_injective:> Inj (=) (=) inject }.
+
 Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}.
 Instance nat_infinite: Infinite nat := {| inject := id |}.
 Instance N_infinite: Infinite N := {| inject_injective := Nat2N.inj |}.
@@ -21,4 +28,4 @@ Section StringFresh.
   Context `{FinCollection string C, ∀ (x: string) (s: C), Decision (x ∈ s)}.
   Global Instance string_fresh: Fresh string C := fresh_generic.
   Global Instance string_fresh_spec: FreshSpec string C := _.
-End StringFresh.
\ No newline at end of file
+End StringFresh.