Commits · public · pactole / coq-pactole

Browse files

Mar 03, 2025
- Coq 8.19 is back + less warning + fix comments · 8c449616
  Lionel Rieg authored 6 months ago
  
  8c449616
Feb 28, 2025
- Removing calls to libhyps and a few cleaning. · 6b86c7c3
  Pierre Courtieu authored 6 months ago
  
  6b86c7c3
Feb 21, 2025
- Extension of MMultiset.map to several base types · fd31a0d7
  Lionel Rieg authored 6 months ago
  
  fd31a0d7
Feb 05, 2025
- Fixing some Proof using. · 6c91f6bc
  Pierre Courtieu authored 7 months ago
  
  6c91f6bc
Nov 22, 2024
- Compatibility with coq 8.20. · 67c4a050
  Pierre Courtieu authored 9 months ago
  67c4a050
Nov 07, 2024
- WIP. · a264ffa5
  Pierre Courtieu authored 10 months ago
  
  a264ffa5
Oct 09, 2024
- Removing the use of some deprecated constants. · d07eb2d6
  Pierre Courtieu authored 11 months ago
  
  d07eb2d6
Oct 08, 2024
- Fix the warning about intuition auto with *. · 9d3c5dd2
  Pierre Courtieu authored 11 months ago
  
  9d3c5dd2
- replacing :> by :: (end) · f624336e
  Pierre Courtieu authored 11 months ago
  
  f624336e
- Replacing "\:>" by "::", in prevision ov coq-8.20 · ca9759ef
  Pierre Courtieu authored 11 months ago
  
  ca9759ef
Oct 07, 2024
- Compiles with coq-8.19 · a373a0b2
  Pierre Courtieu authored 11 months ago
  
  a373a0b2
Jul 23, 2024
- Some cleanup + isobarycenter_3pts -> isobarycenter · 98f303af
  Lionel Rieg authored Jul 23, 2024
  
  98f303af
Jul 22, 2024
- No axiom + unfair case + simplified final statements (similarity_demon) · aae9b5a9
  Lionel Rieg authored Jul 22, 2024
  
  aae9b5a9
Jul 16, 2024
- Cleanup of the proof · f6f7f1a0
  Lionel Rieg authored Jul 16, 2024
  
  f6f7f1a0
Jun 30, 2024
- Proofs for the color bivalent to color bivalent case · 50df062d
  Lionel Rieg authored Jun 30, 2024
  
  50df062d
- Proofs for the color bivalent to not bivalent case · 956c2346
  Lionel Rieg authored Jun 30, 2024
  
  956c2346
Jun 29, 2024
- Proofs for the color bivalent to bivalent case · a12b5bdf
  Lionel Rieg authored Jun 29, 2024
  
  a12b5bdf
Jun 21, 2024
- Adding bivalent_on and color_bivalent_on. · 628d8650
  Pierre Courtieu authored Jun 21, 2024
  
  628d8650
Jun 18, 2024
- Removed an hypothesis from NoDupA_inclA_length_PermutationA · 018806d7
  Lionel Rieg authored Jun 18, 2024
  
  018806d7
Jun 16, 2024
- End of the proof: non color bivalent case + end arguments · d008ced0
  Lionel Rieg authored Jun 16, 2024
  
  d008ced0
Jun 11, 2024
- Distinction between moving and changing inside Formalism.v · 064214ea
  Lionel Rieg authored Jun 11, 2024
  
  064214ea
Jun 10, 2024
- Some tools useful to Even added here as well. · c59c26c6
  Sébastien Bouchard authored Jun 10, 2024
  
  c59c26c6
Jun 06, 2024
- Removal of useless lemma introduced in previous commit · 8558f314
  Sébastien Bouchard authored Jun 6, 2024
  
  8558f314
Jun 05, 2024
- Some proofs to help Even (to be copied in his branch) · 64a03e16
  Sébastien Bouchard authored Jun 5, 2024
  
  64a03e16
May 29, 2024
- Readable proof of round_simplify + sections everywhere (some like it...) · 4e368d06
  Lionel Rieg authored May 29, 2024
  
  4e368d06
May 28, 2024
- Smarter destruct_match tactic · 4cf3526b
  Lionel Rieg authored May 28, 2024
  
  4cf3526b
May 22, 2024
- Roundsimplified finished except th eold part to adapt (again:-(). · f31de730
  Pierre Courtieu authored May 22, 2024
  
  f31de730
Apr 18, 2024
- Half of round_simplified (modulo Lionel :-)). · 20c2a4d2
  Pierre Courtieu authored Apr 18, 2024
  
  20c2a4d2
Apr 03, 2024
- WIP on gathering bivalent: color observation is now a multiset. · 6d78cd64
  Pierre Courtieu authored Apr 3, 2024
  
  6d78cd64
Mar 24, 2024
- Update of the old proof except round_simplify · dfc3e991
  Lionel Rieg authored Mar 24, 2024
  
  dfc3e991
Mar 11, 2024
- Almost finished the compat for the new robogram + pod_Setoid. · f92c9560
  Pierre Courtieu authored Mar 11, 2024
  f92c9560
Mar 01, 2024
- Defining The compat lemmacs for fst and snd vs prod_Setoid. · 1d2df090
  Pierre Courtieu authored Mar 1, 2024
  1d2df090
Jan 08, 2024
- Gathering up to round_simplify (excluded) · 8ef8a425
  Lionel Rieg authored Jan 8, 2024
  
  8ef8a425
Dec 23, 2023
- WithMultiplicityLight done + start of gathering · bc0bddbd
  Lionel Rieg authored Dec 23, 2023
  bc0bddbd
Dec 13, 2023
- Porting Weber case study to coq 8.16. · e7b9451c
  Pierre Courtieu authored Dec 13, 2023
  
  e7b9451c
Sep 13, 2023
- GraphEquivalence.v ported to Coq v8.16 · 9c3743b4
  Lionel Rieg authored Sep 13, 2023
  
  9c3743b4
Aug 25, 2023
- Core setting done, but not case studies · 0bf2af55
  Lionel Rieg authored Aug 25, 2023
  
  0bf2af55
Jun 29, 2023
- Mostly splitting Graph into Graph and ThresholdGraph · 5fe74db2
  Sébastien Bouchard authored Jun 29, 2023
  
  5fe74db2
Apr 03, 2023
- Small improvements · 53cc423a
  Sébastien Bouchard authored Apr 3, 2023
  
  53cc423a
Mar 13, 2023
- Replacement of elim by contradiction · 4a68f3c1
  Sébastien Bouchard authored Mar 13, 2023
  
  4a68f3c1