All pull requests

Pull requests

• Adapt to https://github.com/proux01/rocq/pull/new/fix22547

  #1648·proux01 opened Oct 1, 2026Contributor·

  ·

• Backport packager script changes from Analysis

  #1647·proux01 opened Sep 28, 2026Contributor·

  ·

• Add algebraic_hierarchy.v and numeric_hierarchy.v, and deprecate ssralg.v and ssrnum.v

  #1642·pi8027 opened Aug 26, 2026Member·4 tasks done·

  ·
  2

  20

• preorder for sum

  #1631·StevenSharker opened Jul 24, 2026·4 tasks·

  ·
  5

• Rename the Archimedean mixin and some lemmas (follow-up of #1510)

  kind: clean-up
  #1629·pi8027 opened Jul 20, 2026Member·4 tasks·

  ·

  · 2.8.0

• Compatibility patch for Rocq PR #22272

  #1628·olympichek opened Jul 19, 2026·

  ·

• Generalized compose of linear maps w.r.t. to change of scalar

  kind: enhancement
  #1627·hivert opened Jul 16, 2026Member·1 of 4 tasks·

  ·
  6

• [CI] Add fpseries

  #1623·proux01 opened Jul 6, 2026Contributor·

  ·

• [CI] Add Coq-Combi

  #1616·proux01 opened Jun 25, 2026Contributor·

  ·

• Adapt to HB/mixin-tc

  #1615·Tragicus opened Jun 17, 2026Contributor·4 tasks·

  ·

• reintroducing covariant and tensor product notations

  #1613·hoheinzollern opened Jun 10, 2026Member·4 tasks·

  ·

• spectral: spectral theorem for real symmetric matrices

  #1611·gbdrt opened Jun 5, 2026·4 tasks done·

  ·
  1

• [WIP] Add morphism instances on horner ^~ x

  #1607·pi8027 opened Jun 3, 2026Member·4 tasks·

  ·
  4

• [WIP] Distinguishing scalars from norm codomain

  #1605·CohenCyril opened Jun 2, 2026Member·4 tasks·

  ·
  1

• Use binary parser for rat Number Notation

  #1602·hoheinzollern opened May 28, 2026Member·4 tasks·

  ·
  1

• Add endless and dense orders

  #1597·t6s opened May 13, 2026Member·4 tasks·

  ·
  2

• Refactor the lattice instances on intervals and their bounds

  kind: refactoring
  #1589·pi8027 opened Apr 29, 2026Member·4 tasks·

  ·
  1

• exp -> pow (wip)

  kind: refactoring
  #1544·affeldt-aist opened Feb 24, 2026Member·4 tasks·

  ·

  · 2.7.0
  19

• HB.pack -> HB.enrich

  #1511·gares opened Dec 21, 2025Member·

  ·
  1

• Implemented wrapping of mixin in bigop.v for files monoid.v and nmodule.v

  #1435·CalosciMatteo opened May 19, 2025·4 tasks·

  ·

• Remove the workarounds introduced in #1125

  drops: coq 8.20kind: clean-up
  #1365·pi8027 opened Mar 19, 2025Member·4 tasks·

  ·

  · 2.7.0
  40

• [Draft] Add extended real numbers

  #1338·CohenCyril opened Feb 5, 2025Member·7 tasks·

  ·

  · 2.7.0
  14

• Characteristic for all

  #1308·Tragicus opened Nov 29, 2024Contributor·4 tasks done·

  ·

• Complements to math-comp originating from the trajectories proofs

  #1299·ybertot opened Nov 27, 2024Member·1 of 4 tasks·

  ·

  · 2.7.0
  1

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

  #1213·pi8027 opened Apr 23, 2024Member·2 of 4 tasks·

  ·
  1

  8