Fix bug #4737: cycle tactic doesn't like zero goals.

2 files changed, 15 insertions, 5 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6d7dcb9257..57ff777080 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -660,11 +660,12 @@ let with_shelf tac =
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
 let goodmod p m =
-  let p' = p mod m in
-  (* if [n] is negative [n mod l] is negative of absolute value less
-     than [l], so [(n mod l)+l] is the representative of [n] in the
-     interval [[0,l-1]].*)
-  if p' < 0 then p'+m else p'
+  if m = 0 then 0 else
+    let p' = p mod m in
+    (* if [n] is negative [n mod l] is negative of absolute value less
+      than [l], so [(n mod l)+l] is the representative of [n] in the
+      interval [[0,l-1]].*)
+    if p' < 0 then p'+m else p'
 
 let cycle n =
   let open Proof in
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.