Issues

• Type levels Equality.axioms_.u0 and MonoidProperties.u0 are equated

  math-comp/math-comp#1644 · Filter by author t6s opened on Sep 6, 2026
  5

• TODOs archimedean.v

  math-comp/math-comp#1624 · Filter by author pi8027 opened on Jul 13, 2026

• Rename isCommutativeLaw

  kind: refactoring
  math-comp/math-comp#1609 · Filter by author affeldt-aist opened on Jun 4, 2026

• [Draft] List of "?" tactics

  math-comp/math-comp#1576 · Filter by author CohenCyril opened on Apr 15, 2026
  2

• form -> mxform

  kind: refactoring
  math-comp/math-comp#1574 · Filter by author affeldt-aist opened on Apr 15, 2026

• ltnS vs. ltnSE

  kind: question
  math-comp/math-comp#1573 · Filter by author affeldt-aist opened on Apr 14, 2026

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

  math-comp/math-comp#1569 · Filter by author pi8027 opened on Apr 1, 2026
  1

• Links to corelib broken (since rocq 9.0)

  math-comp/math-comp#1567 · Filter by author gares opened on Mar 25, 2026
  1

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

  math-comp/math-comp#1564 · Filter by author pi8027 opened on Mar 19, 2026
  2

• naming in algebra

  kind: question
  math-comp/math-comp#1557 · Filter by author affeldt-aist opened on Mar 13, 2026
  31

• generalize RHS and LHS

  Feature

  math-comp/math-comp#1555 · Filter by author thery opened on Mar 11, 2026
  2

• rename seq to list

  math-comp/math-comp#1543 · Filter by author affeldt-aist opened on Feb 24, 2026
  1

• use raddf0 with GRing.Scale.law

  kind: question
  math-comp/math-comp#1536 · Filter by author affeldt-aist opened on Feb 13, 2026
  5

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

  math-comp/math-comp#1527 · Filter by author CohenCyril opened on Jan 26, 2026
  1

• imset_set1 should be renamed imset1

  math-comp/math-comp#1522 · Filter by author CohenCyril opened on Jan 16, 2026

• type of x in [gt0 of x]

  kind: documentationkind: question
  math-comp/math-comp#1509 · Filter by author affeldt-aist opened on Dec 2, 2025 · 2.7.0
  2

• Uniformize the name of the re-exportation files

  math-comp/math-comp#1505 · Filter by author pi8027 opened on Nov 28, 2025
  4

  

• Replace HB.lock with Elpi mlock

  math-comp/math-comp#1502 · Filter by author pi8027 opened on Nov 26, 2025
  5

• A semiring morphism structure with a commutativity condition

  math-comp/math-comp#1493 · Filter by author pi8027 opened on Nov 10, 2025

• Generalization and unification of evaluation functions in poly.v

  kind: enhancementkind: refactoring
  math-comp/math-comp#1463 · Filter by author pi8027 opened on Sep 16, 2025

• Document to_multiplicative in the header

  kind: documentation
  math-comp/math-comp#1452 · Filter by author CohenCyril opened on Aug 20, 2025

• Attribute for HB.instance or HB.end: #[ensure = structureName]

  math-comp/math-comp#1432 · Filter by author CalosciMatteo opened on May 15, 2025
  2

• Improving Tips in README.md

  math-comp/math-comp#1396 · Filter by author hoheinzollern opened on Apr 7, 2025

• Some part of the header doc of ssralg is not true anymore

  kind: documentation
  math-comp/math-comp#1390 · Filter by author pi8027 opened on Apr 3, 2025
  1

• Discoverability of rpred* lemmas

  kind: documentation
  math-comp/math-comp#1370 · Filter by author hoheinzollern opened on Mar 26, 2025 · 2.7.0
  3