List view

Remove the pz prefix from (semi)ring and (semi)algebra structures

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

#1487 In math-comp/math-comp;

· pi8027 opened on Oct 21, 2025

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

Naming in archimedean.v

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.

#1377 In math-comp/math-comp;

· affeldt-aist opened on Mar 28, 2025

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

Removing dffun in favor of ffun?

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

[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

More Archimedan lemmas

Status: Draft (not ready).

math-comp/math-compnumber 1510

#1510 In math-comp/math-comp;

· pi8027 opened on Dec 4, 2025

Uniformize the name of the re-exportation files

Status: Open.

#1505 In math-comp/math-comp;

· pi8027 opened on Nov 28, 2025

Split order.v

Status: Open.

#1508 In math-comp/math-comp;

· pi8027 opened on Dec 1, 2025

Order-preserving morphisms

Status: Open.

#1537 In math-comp/math-comp;

· ejgallego opened on Nov 6, 2017