From 26691820328265de9eafaa2adb36fb4619a197fc Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 31 Oct 2017 13:08:51 +0100
Subject: [PATCH] Moved Infinite typeclass to infinite

---
 theories/base.v     | 7 -------
 theories/infinite.v | 9 ++++++++-
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 933535d5..6f02d571 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 79739fbc..dba8a0b9 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.
-- 
GitLab