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

Mentions légales du service

Exceptional GitLab maintenance is scheduled for September 18, 2025. The service will be unavailable between 5:00 and 7:00 pm. Please do not work on the platform until an announcement indicates that maintenance is complete.

Sep 17, 2025
- 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
- Merge pull request #1465 from t6s/doc · eab7793a
  Pierre Roux authored Sep 17, 2025
  eab7793a
- fix typo in ssralg · 15be615f
  Takafumi Saikawa authored Sep 17, 2025
  
  15be615f
Sep 16, 2025
- Adapt mxpoly.v to semimodules, semialgebras, and semilinear functions · 33a2f586
  Kazuhiko Sakaguchi authored Sep 16, 2024
  
  33a2f586
Sep 15, 2025
- Merge pull request #1395 from math-comp/semi-poly · 236861d9
  Kazuhiko Sakaguchi authored Sep 15, 2025
  236861d9
- Merge pull request #1449 from affeldt-aist/unstable_20250816 · c6a65536
  COHEN Cyril authored Sep 15, 2025
  c6a65536
Sep 12, 2025
- two lemmas from MathComp-Analysis' unstable.v · dc84d13d
  Reynald Affeldt authored Aug 16, 2025 and Pierre Roux committed Sep 12, 2025
  
  dc84d13d
- Generalize four lemmas · 7761a69f
  Pierre Roux authored Sep 12, 2025
  
  7761a69f
- Rename bigmax_sup_seq -> bigmaxn_sup_seq · c3019b2f
  Pierre Roux authored Sep 12, 2025
  
  c3019b2f
Sep 06, 2025
- Merge pull request #1460 from proux01/infotheo90 · dd6f0f49
  Reynald Affeldt authored Sep 06, 2025
  dd6f0f49
Sep 05, 2025
- Merge pull request #1459 from proux01/real-closed-drop820 · a950a2eb
  Reynald Affeldt authored Sep 06, 2025
  a950a2eb
- [CI] infotheo now compiles on 9.0 and 9.1 · 7c75e082
  Pierre Roux authored Sep 05, 2025
  
  7c75e082
- Adapt to https://github.com/math-comp/real-closed/pull/80 · 59588f34
  Pierre Roux authored Sep 05, 2025
  
  59588f34
Sep 03, 2025
- Generalize horner_alg to nzSemiRingType · 5f733c26
  Kazuhiko Sakaguchi authored Aug 20, 2025
  
  5f733c26
- Generalize horner_eval and its semilinear function instance to nzSemiRingType · 9223790a
  Kazuhiko Sakaguchi authored Aug 20, 2025
  
  9223790a
- Adapt poly.v to semimodules, semialgebras, and semilinear functions · a8314114
  Kazuhiko Sakaguchi authored Sep 13, 2024
  
  a8314114
- Merge pull request #1457 from proux01/fix-doc · 459bf427
  COHEN Cyril authored Sep 03, 2025
  459bf427
Aug 27, 2025
- Fix doc script · 8f97ab09
  Pierre Roux authored Aug 27, 2025
  
  8f97ab09
- Improvment suggested by CRRRocq · e9190bf8
  COHEN Cyril authored Aug 27, 2025
  e9190bf8
Aug 22, 2025
- Merge pull request #1454 from proux01/cleanup-test · 94fc53d9
  COHEN Cyril authored Aug 22, 2025
  94fc53d9
- Cleanup old test files · ebe8b6a7
  Pierre Roux authored Aug 22, 2025
  
  ebe8b6a7
Aug 21, 2025
- Merge pull request #1453 from proux01/oddorder74 · c0ad2f17
  Quentin Vermande authored Aug 21, 2025
  c0ad2f17
Aug 20, 2025
- Adapt to https://github.com/math-comp/odd-order/pull/74 · 6bf02a11
  Pierre Roux authored Aug 20, 2025
  
  6bf02a11
- Merge pull request #1450 from proux01/ci-update · 18c374d0
  COHEN Cyril authored Aug 20, 2025
  18c374d0
Aug 17, 2025
- [CI] Update Nix toolbox · 38130143
  Pierre Roux authored Aug 17, 2025
  
  38130143
Jul 09, 2025
- Merge pull request #1445 from proux01/ci-update · 93c0bd4d
  Reynald Affeldt authored Jul 10, 2025
  93c0bd4d
- [CI] Add Rocq 9.1+rc1 · 40145a27
  Pierre Roux authored Jul 09, 2025
  
  40145a27
Jul 08, 2025
- lemmas from MathComp-Analysis (when releasing 1.11.0) (#1420) · 8fc66f1a
  Reynald Affeldt authored Jul 08, 2025
  8fc66f1a
Jul 04, 2025
- Merge pull request #1110 from proux01/coq_17876 · bfb9d3b4
  COHEN Cyril authored Jul 04, 2025
  bfb9d3b4
Jul 03, 2025
- Merge pull request #1444 from affeldt-aist/unstable_20250703 · 2ffe6b07
  Pierre Roux authored Jul 03, 2025
  2ffe6b07
- lemmas from MathComp-Analysis' `unstable.v` · 90300c21
  Reynald Affeldt authored Jul 03, 2025
  
  90300c21
Jul 02, 2025
- Merge pull request #1419 from Tragicus/no-new-instance · 21078eb1
  Kazuhiko Sakaguchi authored Jul 02, 2025
  21078eb1
- remove useless instances · 4323ccc2
  Quentin Vermande authored Apr 30, 2025
  
  4323ccc2
- Change level to accept more things in intervals · 7964b15f
  Pierre Roux authored Jun 17, 2025
  
  7964b15f
- Adapt to https://github.com/coq/coq/pull/17876 · cf4d9147
  Pierre Roux authored Oct 12, 2023
  
  cf4d9147
Jul 01, 2025
- Formating · 730595a8
  Pierre Roux authored Feb 28, 2025
  
  730595a8
- Merge pull request #1443 from math-comp/revert-overlay-1438 · a13b240d
  Pierre Roux authored Jul 01, 2025
  a13b240d
- Revert "[CI] Add overlays" · deda5eeb
  Kazuhiko Sakaguchi authored Jul 01, 2025
  deda5eeb
Jun 27, 2025
- Merge pull request #1438 from gares/ssrpat-FO-ignore-imparg · 1892168c
  Pierre Roux authored Jun 27, 2025
  1892168c