Suppress a warning about unused intropatterns

1 files changed, 5 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 07466154c..b635c7e7a 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -604,7 +604,11 @@ Module Z.
 
   Ltac divide_exists_mul := let k := fresh "k" in
   match goal with
-  | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]
+  | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H;
+                              match type of H with
+                              | ex _ => destruct H as [k H]
+                              | _ => destruct H
+                              end
   | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
   end; (omega || auto).