All pull requests

Pull requests

• Clean up Rocq 9.2 compatibility and warning suppressions

  #2453·Alizter opened Nov 8, 2026Collaborator·

  ·
  6

• Characterize bounds of reciprocals, meets and joins in Archimedean ordered fields

  #2447·abooij opened Nov 6, 2026Contributor·

  ·

• Minor improvements around locator (standalone)

  #2432·abooij opened Oct 22, 2026Contributor·

  ·
  3

• Add directed-complete partial orders

  #2431·abooij opened Oct 22, 2026Contributor·

  ·

• Various lemmas around rings.

  #2430·abooij opened Oct 22, 2026Contributor·

  ·
  17

• Real numbers, locators, analysis, metric spaces

  #2426·abooij opened Oct 16, 2026Contributor·3 of 6 tasks·

  ·
  13

• Update coq-scripts for modern Rocq tooling

  #2423·Alizter opened Oct 6, 2026Collaborator·

  ·
  1

• Update developer documentation for Rocq

  #2420·Alizter opened Oct 6, 2026Collaborator·

  ·
  2

• Give Make documentation an explicit root

  #2419·Alizter opened Oct 6, 2026Collaborator·

  ·
  3

• Port developer compiler wrappers to Rocq

  #2415·Alizter opened Oct 6, 2026Collaborator·

  ·
  1

• Make polymorphic inductives cumulative throughout the library

  #2407·Alizter opened Oct 5, 2026Collaborator·4 tasks done·

  ·
  6

• Bicategory (Is1Cat compatible design)

  #2272·patrick-nicodemus opened Apr 1, 2025Contributor·

  ·
  27

• Monoidal coherence

  #2261·patrick-nicodemus opened Mar 20, 2025Contributor·

  ·
  4

• style md add section on bullets

  #2235·Alizter opened Feb 25, 2025Collaborator·

  ·
  1

• building timing reports with dune

  #2234·Alizter opened Feb 25, 2025Collaborator·1 of 3 tasks·

  ·
  3

• subgroups of direct products

  #2233·Alizter opened Feb 25, 2025Collaborator·

  ·
  6

• experiment with HITs and rewritng rules

  #2098·Alizter opened Sep 21, 2024Collaborator·

  ·
  3

• Z-module structure on abelian groups

  #1992·ThomatoTomato opened Jun 11, 2024Collaborator·1 of 4 tasks·

  ·
  16

• biproducts, additive and abelian categories

  #1929·Alizter opened Apr 25, 2024Collaborator·4 of 11 tasks·

  ·
  74

• ci: add whitespace check

  #1881·Alizter opened Mar 6, 2024Collaborator·

  ·
  32

• More H-spaces and Cohomology

  #1875·Alizter opened Feb 25, 2024Collaborator·4 tasks·

  ·
  70

• join construction

  #1860·Alizter opened Feb 19, 2024Collaborator·2 of 4 tasks·

  ·
  27

• remove workaround for coq/coq#8994

  #1807·Alizter opened Jan 12, 2024Collaborator·

  ·
  1

  7

• peano_naturals.v: get rid of universe N

  #1723·jdchristensen opened Feb 25, 2023Collaborator·

  ·
  11

• Try to make entire library Cumulative

  #1710·jdchristensen opened Feb 6, 2023Collaborator·

  ·
  3