List view

Fix the notation scope of function notations in ssralg (#978)

Status: Draft (not ready).

math-comp/math-compnumber 1213

#1213 In math-comp/math-comp;

· pi8027 opened on Apr 23, 2024

Use predicators even extensively

needs: fixPR that needs to be fix (generally because reviewers asked to).PR that needs to be fix (generally because reviewers asked to).

Status: Draft (not ready).

math-comp/math-compnumber 548

#548 In math-comp/math-comp;

· pi8027 opened on Jul 16, 2020

Adding a CODEOWNERS file

Status: Draft (not ready).

math-comp/math-compnumber 709

#709 In math-comp/math-comp;

· CohenCyril opened on Mar 5, 2021

Fix the scope of arguments of intmul

needs: fixPR that needs to be fix (generally because reviewers asked to).PR that needs to be fix (generally because reviewers asked to).

Status: Draft (not ready).

math-comp/math-compnumber 1086

#1086 In math-comp/math-comp;

· proux01 opened on Sep 28, 2023

Avoid exporting warning settings

Status: Open.

#1158 In math-comp/math-comp;

· proux01 opened on Jan 17, 2024

Reducing the number of displayed warnings

kind: buildIssue or PR about the build system/ (Makefile, Dune, ...)Issue or PR about the build system/ (Makefile, Dune, ...)

kind: meta-issueThis issue should be split between several issues, and index them.This issue should be split between several issues, and index them.

Status: Open.

#529 In math-comp/math-comp;

· affeldt-aist opened on Jun 8, 2020

Discoverability of rpred* lemmas

kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...Issue or PR about documentation mistakes, deficiencies, enhancements, ...

Status: Open.

#1370 In math-comp/math-comp;

· hoheinzollern opened on Mar 26, 2025

Change the export control in ssralg but also ssrnum etc to a better and uniform design pattern.

Status: Open.

#1303 In math-comp/math-comp;

· CohenCyril opened on Nov 28, 2024

Inductive principles on set cardinality

Status: Open (in progress).

math-comp/math-compnumber 1120

#1120 In math-comp/math-comp;

· pPomCo opened on Nov 6, 2023

Contrib bigop

needs: rebasePR which is not rebased: check the target is appropriate (generally master) and rebase on top of it.PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it.

Status: Open (in progress).

math-comp/math-compnumber 1119

#1119 In math-comp/math-comp;

· pPomCo opened on Nov 6, 2023

Adding finmap to mathcomp

kind: enhancementIssue or PR about addition of features.Issue or PR about addition of features.

kind: refactoringIssue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)

Status: Draft (not ready).

math-comp/math-compnumber 259

#259 In math-comp/math-comp;

· CohenCyril opened on Dec 10, 2018

WIP galmx : gal_of -> matrix

Status: Draft (not ready).

math-comp/math-compnumber 800

#800 In math-comp/math-comp;

· CohenCyril opened on Oct 14, 2021

Intro discharge subst

Status: Draft (not ready).

math-comp/math-compnumber 502

#502 In math-comp/math-comp;

· CohenCyril opened on May 8, 2020

WIP matrix of a function and base change matrices

Status: Draft (not ready).

math-comp/math-compnumber 801

#801 In math-comp/math-comp;

· CohenCyril opened on Oct 14, 2021

falgebra and fieldext parts of CohenCyril's abel backports

needs: merge of dependenciesPR that depends on another. Documented in the original post of the PR. Review only the increment.PR that depends on another. Documented in the original post of the PR. Review only the increment.

Status: Open (in progress).

math-comp/math-compnumber 1202

#1202 In math-comp/math-comp;

· Tragicus opened on Apr 2, 2024

closed/closure for non-symmetric relations

Status: Draft (not ready).

math-comp/math-compnumber 503

#503 In math-comp/math-comp;

· chdoc opened on May 11, 2020

Contrib finset

Status: Open (in progress).

math-comp/math-compnumber 1118

#1118 In math-comp/math-comp;

· pPomCo opened on Nov 6, 2023

Remove the phantom in tuple

Status: Draft (not ready).

math-comp/math-compnumber 1200

#1200 In math-comp/math-comp;

· CohenCyril opened on Mar 29, 2024

Instances on function types

Status: Open.

#1362 In math-comp/math-comp;

· Tragicus opened on Mar 13, 2025

Complements to math-comp originating from the trajectories proofs

Status: Draft (not ready).

math-comp/math-compnumber 1299

#1299 In math-comp/math-comp;

· ybertot opened on Nov 27, 2024

[Recurring issue] Checking that all new lemmas, Exports modules, and Canonical Structures are exported in ssralg.v

Status: Open.

#440 In math-comp/math-comp;

· ybertot opened on Nov 25, 2019

lra/nra/psatz/ring/field without Stdlib

Status: Open (in progress).

math-comp/math-compnumber 1456

#1456 In math-comp/math-comp;

· proux01 opened on Aug 27, 2025

type of x in [gt0 of x]

kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...Issue or PR about documentation mistakes, deficiencies, enhancements, ...

kind: questionIssue asking a question about math-comp.Issue asking a question about math-comp.

Status: Open.

#1509 In math-comp/math-comp;

· affeldt-aist opened on Dec 2, 2025

about the documentation of preorder.v and order.v

kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...Issue or PR about documentation mistakes, deficiencies, enhancements, ...

Status: Open.

#1516 In math-comp/math-comp;

· affeldt-aist opened on Jan 1, 2026

[Draft] Add extended real numbers

Status: Draft (not ready).

math-comp/math-compnumber 1338

#1338 In math-comp/math-comp;

· CohenCyril opened on Feb 5, 2025