Commits · master · math-comp / math-comp · GitLab

Mentions légales du service

GitLab upgrade completed. Current version is 18.1.6 - https://about.gitlab.com/releases/2025/06/19/gitlab-18-1-released/

Oct 21, 2025
- Merge pull request #1486 from proux01/drop820 · f0a99355
  Kazuhiko Sakaguchi authored Oct 21, 2025
  f0a99355
Oct 17, 2025
- Forgotten file in https://github.com/math-comp/math-comp/pull/1477 · 74c205e0
  Pierre Roux authored Oct 17, 2025
  
  74c205e0
Oct 15, 2025
- Merge pull request #1477 from proux01/rocq21159 · e90518d4
  Pierre Roux authored Oct 15, 2025
  e90518d4
- Merge pull request #1451 from proux01/drop820 · 32a4bdcd
  COHEN Cyril authored Oct 15, 2025
  32a4bdcd
- Replace note by use in deprecations · 3cd29bbc
  Pierre Roux authored Oct 14, 2025
  3cd29bbc
- Remove calls to coqc coqdoc coqmakefile... · 4d2f09c0
  Pierre Roux authored Oct 14, 2025
  
  4d2f09c0
Oct 14, 2025
- Drop support for Coq 8.20 · 25af7b1b
  Pierre Roux authored Oct 14, 2025
  
  25af7b1b
Oct 13, 2025
- Missing comma · c11536cb
  Pierre Roux authored Oct 13, 2025
  
  View commits for tag mathcomp-2.5.0 mathcomp-2.5.0
  
  c11536cb
- Missing last name · b13a1f7d
  Pierre Roux authored Oct 13, 2025
  
  b13a1f7d
- Changelog for 2.5.0 · e9443fd7
  Pierre Roux authored Oct 13, 2025
  
  e9443fd7
- Merge pull request #1466 from math-comp/semi-qpoly · 23e68f58
  Pierre Roux authored Oct 13, 2025
  23e68f58
- Merge pull request #1480 from proux01/ssralg-export · b5dadc4a
  Pierre Roux authored Oct 13, 2025
  b5dadc4a
- Merge pull request #1479 from proux01/revert1462 · 3e830171
  Pierre Roux authored Oct 13, 2025
  3e830171
- Forgotten export in #1444 · ede7abe8
  Pierre Roux authored Oct 13, 2025
  
  ede7abe8
- Revert "Add potentially-zero algebras" · d93d829a
  Pierre Roux authored Oct 13, 2025
  d93d829a
- Adapt `npoly` in `qpoly.v` to semimodules, semialgebras, and semilinear functions · 23a58ae1
  Kazuhiko Sakaguchi authored Sep 16, 2025 and Pierre Roux committed Oct 13, 2025
  
  23a58ae1
- Merge pull request #1462 from math-comp/pzalg · 8ecbea21
  Pierre Roux authored Oct 13, 2025
  8ecbea21
- Add potentially-zero algebras · 2c89547e
  Kazuhiko Sakaguchi authored Sep 15, 2025
  
  2c89547e
Oct 10, 2025
- Merge pull request #1476 from math-comp/semi_closed · 4ebd4d98
  Pierre Roux authored Oct 10, 2025
  4ebd4d98
- Merge pull request #1403 from CohenCyril/eqn_leq_yoneda · f03a913d
  Pierre Roux authored Oct 10, 2025
  f03a913d
Oct 09, 2025
- Helper lemmas to prove (in)equalities · b36235f7
  COHEN Cyril authored Jan 16, 2025 and Pierre Roux committed Oct 09, 2025
  
  b36235f7
Oct 06, 2025
- Adapt to https://github.com/rocq-prover/rocq/pull/21159 · 79818072
  Pierre Roux authored Oct 03, 2025
  
  79818072
Sep 30, 2025
- Add subsemialg_closed and sub(L)SemiAlgType factories · 0bb2a57b
  Kazuhiko Sakaguchi authored Sep 25, 2025
  
  0bb2a57b
Sep 24, 2025
- Adapt to https://github.com/rocq-prover/rocq/pull/20953 (#1474) · 1011f4dd
  Pierre Roux authored Sep 24, 2025
  
  1011f4dd
- Realign conjC and conj_op (#1404) · 7668f9b6
  COHEN Cyril authored Sep 24, 2025
  7668f9b6
Sep 22, 2025
- Merge pull request #1469 from math-comp/rename-archimedean-lemmas · 6d5ffcd0
  Pierre Roux authored Sep 22, 2025
  6d5ffcd0
- Merge pull request #1464 from math-comp/semi-vector · 6601913f
  Pierre Roux authored Sep 22, 2025
  6601913f
- Finalize the renaming of lemmas in archimedean.v · a9637c8a
  Kazuhiko Sakaguchi authored Sep 18, 2025
  
  a9637c8a
- Add semi-vector spaces · a462cf2d
  Kazuhiko Sakaguchi authored Sep 16, 2025
  
  a462cf2d
- Merge pull request #1472 from affeldt-aist/doc_20250922b · 9fe872b6
  Pierre Roux authored Sep 22, 2025
  9fe872b6
- typo · 54c5c358
  Reynald Affeldt authored Sep 22, 2025
  
  54c5c358
- Merge pull request #1471 from affeldt-aist/doc_20250922 · 9c8ccb50
  Pierre Roux authored Sep 22, 2025
  9c8ccb50
Sep 21, 2025
- doc of realDomainType misplaced · ccacfe19
  Reynald Affeldt authored Sep 21, 2025
  
  ccacfe19
Sep 19, 2025
- Merge pull request #1468 from math-comp/num_preds · 14ba97f9
  Pierre Roux authored Sep 19, 2025
  14ba97f9
- Merge pull request #1439 from Tragicus/fingroup_monoid · 39088b9e
  Pierre Roux authored Sep 19, 2025
  39088b9e
Sep 18, 2025
- Rename Rpos, Rneg, Rnneg, Rnpos, and Rreal to pos_num, neg_num, nneg_num,... · 2a101f6a
  Kazuhiko Sakaguchi authored Sep 18, 2025
  2a101f6a
- Merge pull request #1467 from math-comp/scalelinear · 5457f1d2
  COHEN Cyril authored Sep 18, 2025
  5457f1d2
Sep 17, 2025
- Generalize rmorph_comm and some semilinear function instances to the "potentially-zero" case · 8dec5703
  Kazuhiko Sakaguchi authored Sep 17, 2025
  
  8dec5703
- Merge pull request #1455 from CohenCyril/crrrrocq-input · 5a150f60
  COHEN Cyril authored Sep 17, 2025
  5a150f60
- Merge pull request #1269 from math-comp/semi-module-instances · 37562190
  Pierre Roux authored Sep 17, 2025
  37562190