From e1ae086fa401acf1b8c57a22dc9e2a3e380adb84 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Thu, 9 Nov 2017 22:16:33 +0100
Subject: [PATCH] Removed pointless annotation

---
 theories/infinite.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/infinite.v b/theories/infinite.v
index c31d73ac..23767b83 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -71,7 +71,7 @@ Section Fresh.
       apply inbelow; omega.
   Qed.
 
-  Instance fresh_generic: Fresh A C | 20 := λ s, fresh_generic_fix (1 + Nat.log2 (size s)) s 0.
+  Instance fresh_generic: Fresh A C := λ s, fresh_generic_fix s 0.
 
   Instance fresh_generic_spec: FreshSpec A C.
   Proof.
-- 
GitLab