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

Make the finType structure equipped with indexing functions

needs: assigneeIssue or PR that needs an assignee. Please volunteer.Issue or PR that needs an assignee. Please volunteer.

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: Draft (not ready).

math-comp/math-compnumber 317

#317 In math-comp/math-comp;

· pi8027 opened on Apr 1, 2019

Modular lattice of linear subspaces

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

Status: Open.

#613 In math-comp/math-comp;

· pi8027 opened on Oct 11, 2020

[WIP] Make linear subspaces canonically a <code>tbLatticeType</code>

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...)

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 653

#653 In math-comp/math-comp;

· pi8027 opened on Nov 19, 2020

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

[DO NOT MERGE] Attempt to remove dffun

kind: help wantedPR for which help is requested.PR for which help is requested.

Status: Draft (not ready).

math-comp/math-compnumber 745

#745 In math-comp/math-comp;

· pi8027 opened on May 19, 2021

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

Refactor qpoly and poly

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: Open.

#1128 In math-comp/math-comp;

· pi8027 opened on Nov 27, 2023

Discoverability of <code>rpred*</code> 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

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

Removing <code>dffun</code> in favor of <code>ffun</code>?

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

Status: Open.

#701 In math-comp/math-comp;

· strub opened on Mar 2, 2021

WIP galmx : gal_of -&gt; 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 workarounds introduced in #1125

drops: coq 8.20

kind: clean-upThis issure/PR is about cleaning up obsolete code, removing hacks, etcThis issure/PR is about cleaning up obsolete code, removing hacks, etc

Status: Draft (not ready).

math-comp/math-compnumber 1365

#1365 In math-comp/math-comp;

· pi8027 opened on Mar 19, 2025

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