Commit f58a2bfd authored by Guillaume Melquiond's avatar Guillaume Melquiond

New release.

parent ed0ee3e0
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
......
......@@ -109,6 +109,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])
......
......@@ -35,6 +35,7 @@ Variable fexp : Z -> Z.
(** Definition and basic properties about the minimal exponent, when it exists *)
Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
Proof.
intros.
destruct (Z_le_dec x y).
now left.
......
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