Search results

Rename isCommutativeLaw

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.

#1609 In math-comp/math-comp;

· affeldt-aist opened on Jun 4, 2026

[Draft] List of "?" tactics

Status: Open.

#1576 In math-comp/math-comp;

· CohenCyril opened on Apr 15, 2026

form -> mxform

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.

#1574 In math-comp/math-comp;

· affeldt-aist opened on Apr 15, 2026

ltnS vs. ltnSE

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

Status: Open.

#1573 In math-comp/math-comp;

· affeldt-aist opened on Apr 14, 2026

Replace Fact and #[local] Lemma (for internal lemmas) with Let

Status: Open.

#1569 In math-comp/math-comp;

· pi8027 opened on Apr 1, 2026

Links to corelib broken (since rocq 9.0)

Status: Open.

#1567 In math-comp/math-comp;

· gares opened on Mar 25, 2026

Printing issue with the name of structures defined in nmodule.v

Status: Open.

#1564 In math-comp/math-comp;

· pi8027 opened on Mar 19, 2026

naming in algebra

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

Status: Open.

#1557 In math-comp/math-comp;

· affeldt-aist opened on Mar 13, 2026

generalize RHS and LHS

Status: Open.

Feature

#1555 In math-comp/math-comp;

· thery opened on Mar 11, 2026

rename seq to list

Status: Open.

#1543 In math-comp/math-comp;

· affeldt-aist opened on Feb 24, 2026

use raddf0 with GRing.Scale.law

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

Status: Open.

#1536 In math-comp/math-comp;

· affeldt-aist opened on Feb 13, 2026

Replace "Iso..." factories with asset-producing definitions

Status: Open.

#1527 In math-comp/math-comp;

· CohenCyril opened on Jan 26, 2026