Commits · master · CoqInterval / interval · GitLab

Mentions légales du service

Snippets Groups Projects

Git-LFS is now available on our GitLab instance.
Please note that the quota check is now in blocking mode. More informations about quotas: https://gitlab.inria.fr/siteadmin/doc/-/wikis/faq#quota-management-policy-to-monitor-disk-space-by-project-on-gitlab

GitLab upgrade completed. Current version is 17.8.2.

Oct 21, 2024
- New release. · b1693731
  Guillaume Melquiond authored 4 months ago
  
  interval-4.11.1
  
  b1693731
- Tighten enclosure of exponential for inputs greater than 709.78. · a4ba8a8a
  GENEAU DE LAMARLIERE Paul authored 4 months ago and Guillaume Melquiond committed 4 months ago
  
  a4ba8a8a
- Reduce the amount of inference in tactics. · c823cb77
  Guillaume Melquiond authored 4 months ago
  
  c823cb77
- Be more permissive when recognizing "u <= e /\ e <= v". · d8cf8e8e
  Guillaume Melquiond authored 4 months ago
  
  In particular, sharing might be lost due to Coq misfeatures.
  d8cf8e8e
- Fix CI documentation. · a9d77293
  Guillaume Melquiond authored 4 months ago
  
  a9d77293
Aug 26, 2024
- Prove the correctness of the lookup function. · 0f54076c
  Guillaume Melquiond authored 6 months ago
  
  0f54076c
- Update Docker image. · 8cef3276
  Guillaume Melquiond authored 6 months ago
  
  This commit also changes the pipeline so that the build-image job is always executed.
  8cef3276
Aug 23, 2024
- Bump dependencies to comply with Coq >= 8.13 and clean files accordingly. · d6a03b30
  Guillaume Melquiond authored 6 months ago
  
  d6a03b30
- Simplify proof. · 5f642217
  Guillaume Melquiond authored 6 months ago
  
  5f642217
Jun 05, 2024
- New release. · 885fad7f
  Guillaume Melquiond authored 9 months ago
  
  interval-4.11.0
  
  885fad7f
Jun 04, 2024
- Make Coq 8.13.1 the minimal version. · 38ba2cb0
  Guillaume Melquiond authored 9 months ago
  
  38ba2cb0
- Silence warning about duplicate clears. · 56a2e46e
  Guillaume Melquiond authored 1 year ago
  
  56a2e46e
- Add some tests and documentation. · c7c6978f
  Guillaume Melquiond authored 9 months ago
  
  c7c6978f
May 16, 2024
- Work a bit harder to display types. · 0c32d3a0
  Guillaume Melquiond authored 9 months ago
  
  0c32d3a0
- Experiment with some commands for pocket calculations. · 15277128
  Guillaume Melquiond authored 10 months ago
  
  15277128
Apr 25, 2024
- Make proofs a bit more generic. · 0cafdd63
  Guillaume Melquiond authored 10 months ago
  
  0cafdd63
Mar 29, 2024
- Strengthen bounds a bit. · 0d988623
  Guillaume Melquiond authored 11 months ago
  
  0d988623
Mar 19, 2024
- Teach interval about F2R. · dedc3163
  Guillaume Melquiond authored 11 months ago
  
  dedc3163
- Inline proofs and simplify them. · 8b332be1
  Guillaume Melquiond authored 11 months ago
  
  8b332be1
Mar 15, 2024
- Make remove_float a degenerate form of assert_float. · e4f15529
  Guillaume Melquiond authored 11 months ago
  
  e4f15529
Mar 14, 2024
- Rename to assert_float, add remove_float, and simplify proofs. · bd6cdeec
  Guillaume Melquiond authored 11 months ago
  
  bd6cdeec
- Make simplify_wb fail instead of letting it ask for a proof of False. · ad05705d
  Guillaume Melquiond authored 11 months ago
  
  ad05705d
- Linearize proof a bit. · 6512fda4
  Guillaume Melquiond authored 11 months ago
  
  6512fda4
- Merge intermediate lemma into the main proof. · a84834cc
  Guillaume Melquiond authored 11 months ago
  
  a84834cc
- Add a tactic assert_float_transparent. · dc980a03
  Guillaume Melquiond authored 11 months ago
  
  dc980a03
Mar 05, 2024
- New release. · 8c7a5c04
  Guillaume Melquiond authored 1 year ago
  
  interval-4.10.0
  
  8c7a5c04
Feb 22, 2024
- Simplify proofs a bit. · 559c6a54
  Guillaume Melquiond authored 1 year ago
  
  559c6a54
- Add a variant of SF2B a bit easier to use. · b896979d
  Guillaume Melquiond authored 1 year ago
  
  b896979d
Feb 16, 2024
- Factor proof a bit. · b47f25cc
  Guillaume Melquiond authored 1 year ago
  
  b47f25cc
- Add support for integers to remove_floats. · 144942b0
  Guillaume Melquiond authored 1 year ago
  
  144942b0
- Improve remove_floats. · 3c14ea3b
  Guillaume Melquiond authored 1 year ago
  
  3c14ea3b
- Merge lemma about argument reduction and remove some useless definitions. · 33dd1653
  Guillaume Melquiond authored 1 year ago
  
  33dd1653
Feb 09, 2024
- Hide types better and remove some useless definitions. · f49ae518
  Guillaume Melquiond authored 1 year ago
  
  f49ae518
- Simplify proof a bit. · df44bcad
  Guillaume Melquiond authored 1 year ago
  
  df44bcad
Feb 08, 2024
- Fix compilation of plugin with Coq 8.19. · a8b18e81
  Guillaume Melquiond authored 1 year ago
  
  a8b18e81
Feb 07, 2024
- Avoid inefficiency with Coq 8.19. · e41f3aa2
  Guillaume Melquiond authored 1 year ago
  
  e41f3aa2
- Adapt to Coq 8.19 · 775927c7
  Pierre Roux authored 1 year ago and Guillaume Melquiond committed 1 year ago
  
  775927c7
- Add an interval version of the primitive exponential. · 8dd07368
  Guillaume Melquiond authored 1 year ago
  
  8dd07368
- Implement a primitive version of exponential. · ef82328d
  GENEAU DE LAMARLIERE Paul authored 1 year ago and Guillaume Melquiond committed 1 year ago
  
  ef82328d
- Enable the optimized primitives only if the language of expression is available. · d0e677dc
  Guillaume Melquiond authored 1 year ago
  
  d0e677dc