Merge branch 'v8.5'

1 files changed, 6 insertions, 5 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 95e20bc25..45af16759 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -665,11 +665,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