From e9a800321572149f3808e9f68e8e15b6fffa97b2 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 31 Oct 2017 14:11:49 +0100
Subject: [PATCH] Remove uses of 2:
---
theories/infinite.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/infinite.v b/theories/infinite.v
index 25ecb25f..ef4931b8 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -42,8 +42,7 @@ Section Fresh.
Proof.
intros relfg i.
unfold fresh_generic_body.
- destruct decide.
- 2: done.
+ destruct decide; auto.
apply relfg.
Qed.
--
GitLab