Commits · master · Flocq / flocq

23 Jun, 2021 1 commit
- Merge branch 'flocq-3' · 437e1ed6
  Guillaume Melquiond authored Jun 23, 2021
  
  437e1ed6
18 Jun, 2021 1 commit
- New release. · feb5ef18
  Guillaume Melquiond authored Jun 18, 2021
  
  feb5ef18
27 May, 2021 1 commit
- Compatibility with https://github.com/coq/coq/pull/13895 · 239727fc
  Guillaume Melquiond authored May 27, 2021
  
  239727fc
21 May, 2021 1 commit
- compatibility with https://github.com/coq/coq/pull/14037 · b9a5e711
  Andrej Dudenhefner authored May 21, 2021
  
  b9a5e711
12 Apr, 2021 7 commits
- Restore backward compatibility. · b59ca524
  Guillaume Melquiond authored Apr 12, 2021
  
  b59ca524
- Future proof Zaux for https://github.com/coq/coq/pull/14086 · bf633107
  Andrej Dudenhefner authored Apr 08, 2021
  
  bf633107
- Fix opam keywords. · c88bf45c
  Guillaume Melquiond authored Jan 10, 2021
  
  c88bf45c
- Remove the override of omega. · 5ed75e93
  Guillaume Melquiond authored Sep 08, 2020
  
  5ed75e93
- Prove some auxiliary lemmas. · a5fb4129
  Guillaume Melquiond authored Apr 07, 2021
  
  a5fb4129
- Prove some lemmas about Zdigits. · 9140b44d
  Guillaume Melquiond authored Apr 07, 2021
  
  9140b44d
- Move addition overflow to a separate lemma. · c295046a
  Guillaume Melquiond authored Apr 06, 2021
  
  c295046a
03 Apr, 2021 3 commits
- Factor the close-path addition. · cb2e8b32
  Guillaume Melquiond authored Apr 03, 2021
  
  cb2e8b32
- Remove some compatibility notations. · 2babdb74
  Guillaume Melquiond authored Apr 03, 2021
  
  2babdb74
- Make it clearer that SpecFloat is only providing some basic definitions. · 3d5d9098
  Guillaume Melquiond authored Apr 03, 2021
  
  3d5d9098
02 Apr, 2021 4 commits
- Remove automatic exports of ZArith and Reals. · 368dc8ba
  Guillaume Melquiond authored Apr 02, 2021
  
  368dc8ba
- Remove the SpecFloat compatibility layer. · 99532dae
  Guillaume Melquiond authored Apr 02, 2021
  
  99532dae
- Upgrade the minimal supported version of Coq. · 692994a1
  Guillaume Melquiond authored Apr 02, 2021
  
  692994a1
- Prove variant of shl_align_correct. · 898bbbfe
  Guillaume Melquiond authored Apr 02, 2021
  
  898bbbfe
01 Apr, 2021 3 commits
- Add an addition with a proper far path. · 09c940ef
  Guillaume Melquiond authored Apr 01, 2021
  
  09c940ef
- Prove mag_plus_ge. · fec1f233
  Guillaume Melquiond authored Apr 01, 2021
  
  fec1f233
- Prove inbetween_plus_compat. · fc7b8205
  Guillaume Melquiond authored Apr 01, 2021
  
  fc7b8205
10 Jan, 2021 1 commit
- Fix opam keywords. · 87f9f51b
  Guillaume Melquiond authored Jan 10, 2021
  
  87f9f51b
28 Dec, 2020 11 commits
- Simplify proofs a bit. · 43d087f6
  Guillaume Melquiond authored Oct 06, 2020
  
  43d087f6
- Move lemmas around and add some more. · 869faf71
  Guillaume Melquiond authored Oct 06, 2020
  
  869faf71
- Move notations into the proper place. · e0510284
  Guillaume Melquiond authored Oct 06, 2020
  
  e0510284
- Remove the override of omega. · 626b1ba5
  Guillaume Melquiond authored Sep 08, 2020
  
  626b1ba5
- Clean usage of lia. · 5b5c42f9
  Guillaume Melquiond authored Sep 08, 2020
  
  5b5c42f9
- Derive Binary operators from BinarySingleNaN ones. · 8e3860ed
  Guillaume Melquiond authored Sep 08, 2020
  
  8e3860ed
- Improve layout of dependencies a bit. · 7d2bbb8c
  Guillaume Melquiond authored Dec 28, 2020
  
  7d2bbb8c
- Avoid coqdoc warning. · b1730d26
  Guillaume Melquiond authored Dec 28, 2020
  
  b1730d26
- New release. · c9353b99
  Guillaume Melquiond authored Dec 28, 2020
  
  c9353b99
- Replace omega by lia (fix #11 ). · a77bd08b
  Guillaume Melquiond authored Dec 28, 2020
  
  a77bd08b
- Clean opam file. · 4f0f5b26
  Guillaume Melquiond authored Dec 28, 2020
  
  4f0f5b26
24 Dec, 2020 2 commits
- Use lia instead of omega in examples. · 0dc58bee
  Guillaume Melquiond authored Dec 24, 2020
  
  0dc58bee
- Update some examples to newer versions of Coq and Interval. · 8f710128
  Guillaume Melquiond authored Dec 24, 2020
  
  8f710128
23 Dec, 2020 1 commit
- Update some examples to newer versions of Coq and Interval. · 2229829f
  Guillaume Melquiond authored Dec 23, 2020
  
  2229829f
17 Dec, 2020 4 commits
- Test Coq 8.12. · 96ef5e52
  Guillaume Melquiond authored Sep 08, 2020
  
  96ef5e52
- Make REMAKE precious. · f1ba8b48
  Guillaume Melquiond authored Dec 17, 2020
  
  f1ba8b48
- Replace libdir by a dedicated variable, and add support for DESTDIR. · 6a1eda02
  Guillaume Melquiond authored Dec 17, 2020
  
  6a1eda02
- Update remake. · 39a2b8da
  Guillaume Melquiond authored Dec 17, 2020
  
  39a2b8da