Commits · master · CoqInterval / interval

01 Jul, 2022 2 commits
- Update documentation links to Flocq. · 1d5ddb99
  Guillaume Melquiond authored Jul 01, 2022
  
  1d5ddb99
- Reset owner and group of distributed files. · a7d16b17
  Guillaume Melquiond authored Jul 01, 2022
  
  a7d16b17
22 Apr, 2022 2 commits
- Make Fadd_fast closer to Flocq's reference implementation. · 68501e8e
  Guillaume Melquiond authored Apr 21, 2022
  
  68501e8e
- Do not renormalize short mantissas. · 8c9f8620
  Guillaume Melquiond authored Apr 21, 2022
  
  8c9f8620
15 Apr, 2022 1 commit
- Build all the packages at once. · 5e8f8e0a
  Guillaume Melquiond authored Apr 15, 2022
  
  5e8f8e0a
14 Apr, 2022 1 commit
- New release. · b6fdc261
  Guillaume Melquiond authored Apr 14, 2022
  
  b6fdc261
02 Apr, 2022 2 commits
- Precompute the goal bounds. · e584dcfa
  Guillaume Melquiond authored Apr 02, 2022
  
  e584dcfa
- Do not compare widths when the intervals are unbounded. · d725361c
  Guillaume Melquiond authored Apr 02, 2022
```
As a side effect, the bisection now happens on the output interval instead
of the input interval. This might make refinement a bit faster in case of
bisection.
```
  d725361c
30 Mar, 2022 7 commits
- Restore the still relevant part of the CI documentation. · d52b6fe6
  Guillaume Melquiond authored Mar 30, 2022
  
  d52b6fe6
- Add a script to ease translating the examples into HTML. · 0d63b759
  Guillaume Melquiond authored Mar 30, 2022
  
  0d63b759
- Improve documentation a bit. · ef3a41c8
  Guillaume Melquiond authored Mar 30, 2022
  
  ef3a41c8
- New release. · b2f2a7f3
  Guillaume Melquiond authored Mar 30, 2022
  
  b2f2a7f3
- Update documentation. · 4218e71a
  Guillaume Melquiond authored Mar 30, 2022
  
  4218e71a
- Remove the two-argument version of "root" and use "i_autodiff" instead. · 3064846e
  Guillaume Melquiond authored Mar 30, 2022
  
  3064846e
- Add a "root_intro" tactic as well as a freestanding "root" tactic. · 26ca514a
  Guillaume Melquiond authored Mar 30, 2022
  
  26ca514a
29 Mar, 2022 3 commits
- Add a helper function for root_intro. · 8a813f74
  Guillaume Melquiond authored Mar 29, 2022
  
  8a813f74
- Teach I.subset, I.meet, and I.join, about empty intervals. · 8cf7ad05
  Guillaume Melquiond authored Mar 29, 2022
  
  8cf7ad05
- Give I.subset_correct its proper statement. · e6bfad66
  Guillaume Melquiond authored Mar 29, 2022
  
  e6bfad66
08 Mar, 2022 2 commits
- Update URLs. · 5ffa1a32
  Guillaume Melquiond authored Mar 08, 2022
  
  5ffa1a32
- Update CI. · 5f9768ea
  Guillaume Melquiond authored Mar 08, 2022
  
  5f9768ea
06 Mar, 2022 1 commit
- Use a bisection algorithm for root finding. · 342766a6
  Guillaume Melquiond authored Mar 06, 2022
  
  342766a6
05 Mar, 2022 2 commits
- Add support for empty intervals during goal checking. · 4e8a5145
  Guillaume Melquiond authored Mar 05, 2022
  
  4e8a5145
- Add I.is_empty. · 5ef262cc
  Guillaume Melquiond authored Mar 05, 2022
  
  5ef262cc
04 Mar, 2022 5 commits
- Add a tactic for root finding. · 9ee8aa80
  Guillaume Melquiond authored Mar 04, 2022
  
  9ee8aa80
- Add a helper tactic for applying a Newton iteration. · 1850ab34
  Guillaume Melquiond authored Mar 04, 2022
  
  1850ab34
- Remove redundant scan. · 169bf001
  Guillaume Melquiond authored Mar 04, 2022
  
  169bf001
- Look for variables earlier, in case they are valid terms. · 732cd115
  Guillaume Melquiond authored Mar 04, 2022
  
  732cd115
- Prove an algorithm for a Newton refinement. · 371b9e17
  Guillaume Melquiond authored Mar 04, 2022
  
  371b9e17
03 Mar, 2022 7 commits
- Avoid some pointless interval multiplications. · 706371df
  Guillaume Melquiond authored Mar 03, 2022
  
  706371df
- Replace I.div with I.inv when possible. · e8992295
  Guillaume Melquiond authored Mar 03, 2022
  
  e8992295
- Improve behavior of exp in case of overflow. · dbd5bbf6
  Guillaume Melquiond authored Mar 03, 2022
  
  dbd5bbf6
- Add a silent version of I.inv. · c783a5bd
  Guillaume Melquiond authored Mar 03, 2022
  
  c783a5bd
- Add example. · e394d618
  Guillaume Melquiond authored Mar 03, 2022
  
  e394d618
- Recognize Rpower without having to unfold it first. · 52213103
  Guillaume Melquiond authored Mar 02, 2022
  
  52213103
- Improve the heuristic for detecting variables and unfoldable definitions. · f497c4b7
  Guillaume Melquiond authored Mar 02, 2022
  
  f497c4b7
15 Jan, 2022 2 commits
- New release. · bb881eb7
  Guillaume Melquiond authored Jan 15, 2022
  
  bb881eb7
- Add degenerate forms of interval_intro and integral_intro. · bf8ee1da
  Guillaume Melquiond authored Jan 15, 2022
  
  bf8ee1da
14 Dec, 2021 1 commit
- Ensure compatibility with Coq 8.15. · db1c36ca
  Guillaume Melquiond authored Dec 14, 2021
  
  db1c36ca
08 Nov, 2021 2 commits
- New release. · ac58af4a
  Guillaume Melquiond authored Nov 08, 2021
  
  ac58af4a
- Update the upper bound on dependencies. · 1d5f9fa5
  Guillaume Melquiond authored Nov 08, 2021
  
  1d5f9fa5