gitlab.inria.fr / flocq/flocq / commits
| SHA | Message | Author | Date | Stats |
|---|---|---|---|---|
| 8ca92d39 | Make reduction behave a bit better. | Guillaume Melquiond <g****d@i****r> | 2 months ago | |
| 7aab8f55 | New release. | Guillaume Melquiond <g****d@i****r> | 7 months ago | |
| f1ee7c79 | Move remake.cpp out of the way. | Guillaume Melquiond <g****d@i****r> | 7 months ago | |
| 05badc52 | Use a custom implementation of coqdep. | Guillaume Melquiond <g****d@i****r> | 7 months ago | |
| c307f1c9 | Remove obsolete files. | Guillaume Melquiond <g****d@i****r> | 7 months ago | |
| 54cadd27 | Prevent Coqdep from polluting dependencies. | Guillaume Melquiond <g****d@i****r> | 11 months ago | |
| 2d8fe5d9 | merge Merge branch 'rm-dots' into 'master' | Guillaume Melquiond <g****d@i****r> | about 1 year ago | |
| 46227e39 | Remove useless `...` | Gaëtan Gilbert <g****t@s****t> | about 1 year ago | |
| d0875fdb | Update external links in generated documentation. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| eb095cfd | Remove some warnings. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 52deacc3 | Update Docker image. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| fab16db5 | Replace deprecated alias Zmod with Z.modulo. |
Andres Erbsen <a****r@m****u>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 1 year ago | |
| e1443068 | New release. | Guillaume Melquiond <g****d@i****r> | over 1 year ago | |
| 0a685a5c | Partially revert "Adapt to https://github.com/coq/coq/pull/19530" | Pierre Roux <p****x@o****r> | over 1 year ago | |
| 41ad3225 | Clean some proofs. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| 5f164739 | Simplify statement and proof of le_shr_le. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| c3b76b7d | Reduce amount of warnings. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| d782e8de | merge Merge branch 'stdlib_repo' into 'master' | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| f210ddc7 | Update Docker image. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| c91b008e | Remove the need for NEW_BUILD_IMAGE. | Guillaume Melquiond <g****d@i****r> | almost 2 years ago | |
| f22fcb26 | Bump Coq min version to 8.15 and associated cleanups |
Pierre Roux <p****x@o****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
about 2 years ago | |
| b18b7647 | Bump Coq min version to 8.14 and associated cleanups |
Pierre Roux <p****x@o****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
about 2 years ago | |
| d8a6fcab | Adapt to https://github.com/coq/coq/pull/19530 |
Pierre Roux <p****x@o****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
about 2 years ago | |
| cb07ce50 | Simplify proofs a bit. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| c85132b8 | New release. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| 1deaa7fe | Add a proof-free variant of SF2B. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| e58d998b | Fix missing file from install/clean. | Guillaume Melquiond <g****d@i****r> | about 2 years ago | |
| 561210b4 | adapt to coq/coq#18729 |
Andres Erbsen <a****b@a****s>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 2 years ago | |
| 1c4af8ad | Prove pred_FLX_exact_shift and pred_FLT_exact_shift. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| c5f475dd | New release. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 913ce5c3 | Fix constructor name. | Guillaume Melquiond <g****d@i****r> | over 2 years ago | |
| 3e8b2e09 | merge Merge branch 'coq_18164' into 'master' | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 3a59324f | Adapt to https://github.com/coq/coq/pull/18164 | Pierre Roux <p****x@o****r> | almost 3 years ago | |
| 51624684 | New release. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| 0e6066f0 | Avoid leaking dummy compatibility symbols. | Guillaume Melquiond <g****d@i****r> | almost 3 years ago | |
| fb3c1a79 | New release. | Guillaume Melquiond <g****d@i****r> | about 3 years ago | |
| 7925c219 | Update continuous integration. | Guillaume Melquiond <g****d@i****r> | about 3 years ago | |
| a84196ad | Update homepage URL. | Guillaume Melquiond <g****d@i****r> | about 3 years ago | |
| 3fd35c38 | Fix missing build dependencies. | Guillaume Melquiond <g****d@i****r> | about 3 years ago | |
| 2c499dc6 | merge Merge branch 'coq_16920' into 'master' | Guillaume Melquiond <g****d@i****r> | over 3 years ago | |
| 41d38dfc | Adapt to https://github.com/coq/coq/pull/16920 | Pierre Roux <p****x@o****r> | over 3 years ago | |
| eb9be7d3 | New release. | Guillaume Melquiond <g****d@i****r> | over 3 years ago | |
| 0b6c5f10 | Prevent loading of Coq's user configuration. | Guillaume Melquiond <g****d@i****r> | over 3 years ago | |
| e18cdc28 | merge Merge branch 'deprecate-elim-case-type-2' into 'master' | Guillaume Melquiond <g****d@i****r> | over 3 years ago | |
| f1845124 | Adapt w.r.t. coq/coq#16904 (again). | Pierre-Marie Pédrot <p****t@i****r> | over 3 years ago | |
| bf07aa7f | merge Merge branch 'deprecate-elim-case-type' into 'master' | Guillaume Melquiond <g****d@i****r> | almost 4 years ago | |
| 19b2f7ec | Adapt w.r.t. coq/coq#16904. | Pierre-Marie Pédrot <p****t@i****r> | almost 4 years ago | |
| 3c92e3f9 | Ensure compatibility with Coq's PR 16293. | Guillaume Melquiond <g****d@i****r> | about 4 years ago | |
| 445ea0ff | Properly handle the compatibility files. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| c96f0422 | merge Merge branch 'flocq-3' | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 0188199c | New release. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 0fc92743 | Remove the BSN alias, as it confuses Coq's extraction mechanism. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| d648041e | merge Merge branch 'flocq-3' | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 5510a80f | Add Bnearbyint and Btrunc. |
Paul Geneau <p****e@e****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 4 years ago | |
| ec7ea911 | Prove inbetween_float_NA_sign. |
Paul Geneau <p****e@e****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 4 years ago | |
| cdcd92b7 | Prove Zdigits_succ_le. |
Paul Geneau <p****e@e****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 4 years ago | |
| 1d5cf2ac | Prove Rlt_bool_cond_Ropp. |
Paul Geneau <p****e@e****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 4 years ago | |
| e81ae57d | Prove Ztrunc_div. |
Paul Geneau <p****e@e****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 4 years ago | |
| 81ec26b3 | Update CI. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 87af079a | Prove cond_Zopp_0. |
Paul Geneau <p****e@e****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 4 years ago | |
| 792f4a3a | merge Merge branch 'coq_15754' into 'flocq-3' | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| ef9d501a | Adapt to https://github.com/coq/coq/pull/15754 | Pierre Roux <p****e@r****r> | over 4 years ago | |
| 5a9d2d34 | Remove some compatibility lemmas. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 3af469f4 | Simplify proofs a bit. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| ef12d4a7 | Prove Beqb_refl. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 56addf5c | Fix compilation issues. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 55e006e4 | Change check-more so that it compiles files using the installed libraries. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 32db7151 | Clean proof. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| cc5372fb | Add helper canonical_bounded. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 44236b02 | Relate canonical exponent and order. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| c81b1f10 | Improve compatibility with Coq 8.16. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| a8de4a9c | merge Merge branch 'flocq-3' | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 088acf93 | New release. | Guillaume Melquiond <g****d@i****r> | over 4 years ago | |
| 1423a6d3 | merge Merge branch 'print17' into 'master' | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| 09d83571 | Decimal printing of binary64 with 17 digits is enough | Pierre Roux <p****e@r****r> | almost 5 years ago | |
| 311182de | New release. | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| e68658cb | Compatibility with Coq 8.15. |
Kazuhiko Sakaguchi <p****7@g****m>
Committed by: Guillaume Melquiond <g****d@i****r> |
almost 5 years ago | |
| b8652003 | Compatibility with Coq 8.15. |
Kazuhiko Sakaguchi <p****7@g****m>
Committed by: Guillaume Melquiond <g****d@i****r> |
almost 5 years ago | |
| 4a37ff45 | Clean code a bit. | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| 117c4d0a | Remove INR from Pff. | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| 7a697420 | Update Coq versions. | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| 138f34bf | merge Merge branch 'flocq-3' | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| dc95fa7f | Silence warning. | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| d26acf9f | Add a rule to install .glob files (fix #19). | Guillaume Melquiond <g****d@i****r> | almost 5 years ago | |
| b20cb064 | Silence warning (fix #18). |
Xavier Leroy <x****y@c****r>
Committed by: Guillaume Melquiond <g****d@i****r> |
almost 5 years ago | |
| a40e7487 | Adapt to coq/coq#14819 | Pierre Roux <p****x@o****r> | about 5 years ago | |
| ca655d25 | New release. | Guillaume Melquiond <g****d@i****r> | about 5 years ago | |
| 63ae222c | Restore compilation with Coq 8.11 | Pierre Roux <p****e@r****r> | about 5 years ago | |
| feb5ef18 | New release. | Guillaume Melquiond <g****d@i****r> | about 5 years ago | |
| 239727fc | Compatibility with https://github.com/coq/coq/pull/13895 | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| b9a5e711 | compatibility with https://github.com/coq/coq/pull/14037 | Andrej Dudenhefner <m****i@g****m> | over 5 years ago | |
| b59ca524 | Restore backward compatibility. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| bf633107 | Future proof Zaux for https://github.com/coq/coq/pull/14086 |
Andrej Dudenhefner <m****i@g****m>
Committed by: Guillaume Melquiond <g****d@i****r> |
over 5 years ago | |
| a5fb4129 | Prove some auxiliary lemmas. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| 9140b44d | Prove some lemmas about Zdigits. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| c295046a | Move addition overflow to a separate lemma. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| cb2e8b32 | Factor the close-path addition. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| 2babdb74 | Remove some compatibility notations. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| 3d5d9098 | Make it clearer that SpecFloat is only providing some basic definitions. | Guillaume Melquiond <g****d@i****r> | over 5 years ago | |
| 368dc8ba | Remove automatic exports of ZArith and Reals. | Guillaume Melquiond <g****d@i****r> | over 5 years ago |