Remove uses of 2:

e9a80032 · Johannes Kloos · a62a60ae · e9a80032
Commit e9a80032 authored Oct 31, 2017 by Johannes Kloos
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 2 deletions

theories/infinite.v theories/infinite.v +1 -2

No files found.
--- 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.