Commit b1926d22 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'flocq-2.5'

parents 3aac99c3 f58a2bfd
Version 2.5.2:
- ensured compatibility from Coq 8.4 to 8.6
Version 2.5.1:
- ensured compatibility with both Coq 8.4 and 8.5
......
......@@ -110,6 +110,7 @@ dist: $(EXTRA_DIST)
for f in $(REMOVE_FROM_DIST) ; do rm -rf $PACK/$f; done
git log --pretty="format:%ad %s" --date=short > $PACK/ChangeLog
cat /dev/null > $PACK/ChangeLog
rm $PACK/.mailmap
rm `find $PACK -name .gitignore`
tar czf $PACK.tar.gz $PACK
rm -rf $PACK
AC_INIT([Flocq], [2.5.1],
AC_INIT([Flocq], [2.5.2],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......
......@@ -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