Commits · 6b86c7c3e270afc131d31a14fefea6a6c47a297d · pactole / coq-pactole

Feb 28, 2025
- Removing calls to libhyps and a few cleaning. · 6b86c7c3
  Pierre Courtieu authored 4 months ago
  
  6b86c7c3
Nov 26, 2024
- Removing the paper (moved to the sapporo repo. · e02bad43
  Pierre Courtieu authored 7 months ago
  
  e02bad43
Nov 25, 2024
- Merge remote-tracking branch 'origin/coq-8.16' into weber · a70e1a0c
  Pierre Courtieu authored 7 months ago
```
Merging coq-8.20 adjustments to weber branch.
```
  a70e1a0c
Nov 22, 2024
- Merge branch 'coq-8.16' of https://gitlab.liris.cnrs.fr/xurbain/pactole-dev into coq-8.16 · 9d7d3d3c
  Pierre Courtieu authored 7 months ago
  
  9d7d3d3c
- Compatibility with coq 8.20. · 67c4a050
  Pierre Courtieu authored 7 months ago
```
coq 8.20 has a small regression with lia.
+ some small stdlib changes.
```
  67c4a050
Nov 21, 2024
- Fixing the Print Assumption on Weber proofs. · 50e1eb0e
  Pierre Courtieu authored 7 months ago
```
Which amount to discovering a bug in Coq and work around it.
```
  50e1eb0e
Nov 19, 2024
- Fix of other proofs about Weber point. · 466d47b2
  Pierre Courtieu authored 7 months ago
  
  466d47b2
- Merg with master · 0631003b
  Pierre Courtieu authored 7 months ago
  
  0631003b
- All unnecessaru axioms proved. But Print Assumptions segfaults. · 66d83a75
  Pierre Courtieu authored 7 months ago
  
  66d83a75
Nov 18, 2024
- Last admits for Weber point. · cf5ba5b9
  Pierre Courtieu authored 7 months ago
  
  cf5ba5b9
Nov 13, 2024
- WIP. One admit removed. · 09a1ab7d
  Pierre Courtieu authored 7 months ago
  
  09a1ab7d
Nov 07, 2024
- WIP. · a264ffa5
  Pierre Courtieu authored 7 months ago
  
  a264ffa5
Nov 06, 2024
- Another admit solved. WIP. · 6e08a8ac
  Pierre Courtieu authored 7 months ago
  
  6e08a8ac
- One admit removed. WIP. · 9f7e1189
  Pierre Courtieu authored 7 months ago
  
  9f7e1189
Nov 05, 2024
- several more admits removed. · 51ea3d62
  Pierre Courtieu authored 7 months ago
  
  51ea3d62
Oct 28, 2024
- Compatibility with coq 8.18-8.19. Merge branch 'coq-8.16'. · 2c38510a
  Pierre Courtieu authored 8 months ago
  
  2c38510a
Oct 25, 2024
- Removing the type class for number of robots. · 3e88b516
  Pierre Courtieu authored 8 months ago
```
This is to be discussed. Let us leave it as before for now.
```
  3e88b516
- Merge remote-tracking branch 'origin/prod' into coq-8.16 · 41dc107c
  Pierre Courtieu authored 8 months ago
  
  41dc107c
Oct 18, 2024
- A few more steps proved thanks to a brainstorming in Tokyo! · c4c78c7f
  Pierre Courtieu authored 8 months ago
  
  c4c78c7f
- WIP on last proofs about WB point. · dc3672c2
  Pierre Courtieu authored 8 months ago
  
  dc3672c2
Oct 09, 2024
- Removing the use of some deprecated constants. · d07eb2d6
  Pierre Courtieu authored 8 months ago
  
  d07eb2d6
Oct 08, 2024
- Fix the warning about intuition auto with *. · 9d3c5dd2
  Pierre Courtieu authored 8 months ago
  
  9d3c5dd2
- Silenced the non uniform inheritance warning · 44017fa8
  Pierre Courtieu authored 8 months ago
```
+ 1 occurrence of  :> -> ::
```
  44017fa8
- replacing :> by :: (end) · f624336e
  Pierre Courtieu authored 8 months ago
  
  f624336e
- Replacing "\:>" by "::", in prevision ov coq-8.20 · ca9759ef
  Pierre Courtieu authored 8 months ago
  
  ca9759ef
Oct 07, 2024
- Compiles with coq-8.19 · a373a0b2
  Pierre Courtieu authored 8 months ago
  
  a373a0b2
- Compiles with coq-8.16. · e05fe024
  Pierre Courtieu authored 8 months ago
  
  e05fe024
Jun 16, 2024
- Update .gitlab-ci.yml file · d5c7ac43
  Xavier Urbain authored 1 year ago and Sébastien Bouchard committed 1 year ago
  
  d5c7ac43
Jun 12, 2024
- Update .gitlab-ci.yml file · 552e084b
  Xavier Urbain authored 1 year ago
  
  552e084b
Jun 10, 2024
- Some tools useful to Even added here as well. · c59c26c6
  Sébastien Bouchard authored 1 year ago
  
  c59c26c6
Jun 06, 2024
- Removal of useless lemma introduced in previous commit · 8558f314
  Sébastien Bouchard authored 1 year ago
  
  8558f314
Jun 05, 2024
- Some proofs to help Even (to be copied in his branch) · 64a03e16
  Sébastien Bouchard authored 1 year ago
  
  64a03e16
Feb 19, 2024
- removed empty coq file · d371c464
  MathisBD authored 1 year ago
  
  d371c464
- cleanup · da41a3f8
  MathisBD authored 1 year ago
  
  da41a3f8
Feb 18, 2024
- proof of weber_aligned_spec_weak · 81473bf8
  MathisBD authored 1 year ago
  
  81473bf8
- proof of weber_majority_weak · 075ab33e
  MathisBD authored 1 year ago
  
  075ab33e
- finished technical lemmas about derivation · d0e91e46
  MathisBD authored 1 year ago
  
  d0e91e46
Feb 16, 2024
- finished proof of weber_first_order · d9141082
  MathisBD authored 1 year ago
  
  d9141082
Feb 15, 2024
- proof of deriv_neg_not_weber · 02dee4fb
  MathisBD authored 1 year ago
  
  02dee4fb
Feb 13, 2024
- push_negs first version · cd82d629
  MathisBD authored 1 year ago
  
  cd82d629