From 9b2beca375e1b3fd8f1298ee13656124fe24e807 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 17:45:04 +0200
Subject: Fix bug #4737: cycle tactic doesn't like zero goals.

---
 test-suite/bugs/closed/4737.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/4737.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4737.v b/test-suite/bugs/closed/4737.v
new file mode 100644
index 0000000000..84ed45e454
--- /dev/null
+++ b/test-suite/bugs/closed/4737.v
@@ -0,0 +1,9 @@
+Goal True.
+Proof.
+exact I; cycle 1.
+Qed.
+
+Goal True.
+Proof.
+exact I; swap 1 2.
+Qed.
-- 
cgit v1.2.3