Commits · master · CoqInterval / interval

30 Apr, 2020 11 commits
- Update documentation. · 540621b2
  Guillaume Melquiond authored Apr 30, 2020
  
  540621b2
- Add an example for multi-dimensional bisection. · 6fd0f03f
  Guillaume Melquiond authored Apr 30, 2020
  
  6fd0f03f
- Replace map_nth by nth_map. · c7810788
  Guillaume Melquiond authored Apr 30, 2020
  
  c7810788
- Move change_nth out of IntervalAlgos. · b49adf09
  Guillaume Melquiond authored Apr 30, 2020
  
  b49adf09
- Simplify contains_all a bit. · 71f7b3fc
  Guillaume Melquiond authored Apr 30, 2020
  
  71f7b3fc
- Remove unused definitions. · 04315527
  Guillaume Melquiond authored Apr 30, 2020
  
  04315527
- Do not distinguish between naive evaluation and bisection; always use the latter. · e04bf9d9
  Guillaume Melquiond authored Apr 30, 2020
  
  e04bf9d9
- Make "i_depth 0" perform one step of computations. · b9c1e150
  Guillaume Melquiond authored Apr 30, 2020
  
  b9c1e150
- Split i_bisect from i_bisect_diff and i_bisect_taylor. Allow several i_bisect options. · 7332834a
  Guillaume Melquiond authored Apr 30, 2020
  
  7332834a
- Make bisection algorithms multi-dimensional. · 7c2f9c92
  Guillaume Melquiond authored Apr 30, 2020
  
  7c2f9c92
- Add a bisect function to split intervals into two halves. · abe88bd6
  Guillaume Melquiond authored Apr 30, 2020
  
  abe88bd6
29 Apr, 2020 3 commits
- Get rid of bound_proof. · 2ea56f70
  Guillaume Melquiond authored Apr 29, 2020
  
  2ea56f70
- Remove unused definitions. · dd8b6d35
  Guillaume Melquiond authored Apr 29, 2020
  
  dd8b6d35
- Remove unused definitions. · fd5f6d90
  Guillaume Melquiond authored Apr 29, 2020
  
  fd5f6d90
28 Apr, 2020 9 commits
- Test integral_intro. · ed27dec0
  Guillaume Melquiond authored Apr 28, 2020
  
  ed27dec0
- Clean outdated snippets. · ab2c668d
  Guillaume Melquiond authored Apr 28, 2020
  
  ab2c668d
- Add tactic inegral_intro. · 2dca6600
  Guillaume Melquiond authored Apr 28, 2020
  
  2dca6600
- Make eval_RInt_gen a bit more versatile. · 39ce6460
  Guillaume Melquiond authored Apr 28, 2020
  
  39ce6460
- Make eval_RInt a bit more versatile. · 2972dade
  Guillaume Melquiond authored Apr 28, 2020
  
  2972dade
- Make code a bit clearer. · 7a9abbbe
  Guillaume Melquiond authored Apr 28, 2020
  
  7a9abbbe
- Factor computation code a bit. · 743d55d9
  Guillaume Melquiond authored Apr 28, 2020
  
  743d55d9
- Make reification a bit more robust. · 4c0ef80d
  Guillaume Melquiond authored Apr 28, 2020
  
  4c0ef80d
- Factor reification of RInt a bit. · 4389befb
  Guillaume Melquiond authored Apr 28, 2020
  
  4389befb
05 Apr, 2020 9 commits
- Avoid some deprecation warnings. · a6047ec7
  Guillaume Melquiond authored Apr 05, 2020
  
  a6047ec7
- Resolve links to Coquelicot. · bf9e5e5d
  Guillaume Melquiond authored Apr 05, 2020
  
  bf9e5e5d
- Deploy documentation. · e96eb6e9
  Guillaume Melquiond authored Apr 05, 2020
  
  e96eb6e9
- Change the minimal version for Flocq to 3.1. · a3d07fb8
  Guillaume Melquiond authored Apr 05, 2020
  
  a3d07fb8
- Change the minimal Coq version to 8.8. · 0b5be8f0
  Guillaume Melquiond authored Apr 05, 2020
```
This commit also makes the SSReflect version requirements more explicit.
```
  0b5be8f0
- Fix compilation. · 3cef6010
  Guillaume Melquiond authored Apr 05, 2020
  
  3cef6010
- Merge branch 'interval-3.4' · a3c67670
  Guillaume Melquiond authored Apr 05, 2020
  
  a3c67670
- Add continuous integration. · 61ce0414
  Guillaume Melquiond authored Apr 05, 2020
  
  61ce0414
- Simplify archive generation. · 04df7d7c
  Guillaume Melquiond authored Apr 05, 2020
  
  04df7d7c
25 Feb, 2020 3 commits
- New release. · 3bf5beb5
  Guillaume Melquiond authored Feb 25, 2020
  
  3bf5beb5
- Ensure compatibility with Coq 8.11. · 6fcdacfb
  Guillaume Melquiond authored Feb 25, 2020
  
  6fcdacfb
- Remove useless file. · 0157755b
  Guillaume Melquiond authored Feb 25, 2020
  
  0157755b
09 Dec, 2019 5 commits
- Remove unused function F.round. · ec99901a
  Guillaume Melquiond authored Dec 09, 2019
  
  ec99901a
- Precompute scaling factors. · 56bee29c
  Guillaume Melquiond authored Dec 09, 2019
  
  56bee29c
- Remove obsolete tests. · 102d9541
  Guillaume Melquiond authored Dec 09, 2019
  
  102d9541
- Remove unused theorem sqr_ge_0. · 604322b3
  Guillaume Melquiond authored Dec 09, 2019
  
  604322b3
- Add F.fromZ_DN and F.fromZ_UP. · beb91bc3
  Guillaume Melquiond authored Dec 09, 2019
```
F.fromZ is still available but its result is specified only for small
integer inputs.
```
  beb91bc3