Commit 084ef5ec authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensure compatibility with Coq 8.6.

parent a25651ae
......@@ -853,7 +853,7 @@ Proof.
intros n Zn.
rewrite <- (Zdigits_abs n).
assert (Hn: (0 < Zabs n)%Z).
destruct n ; try easy.
destruct n ; [|easy|easy].
now elim Zn.
destruct (Zabs n) as [|p|p] ; try easy ; clear.
simpl.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment