All pull requests

Pull requests

• More on compact types

  #2434·thchatzidiamantis opened Oct 25, 2026Contributor·

  ·
  14

• Overture: make paths_rew* unfold with simpl/cbn; add tests

  #2433·jdchristensen opened Oct 25, 2026Collaborator·

  ·

• 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·

  ·
  1

• Minor cleanup of the rationals

  #2428·abooij opened Oct 22, 2026Contributor·

  ·

• 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

• Remove obsolete pattern settings safely

  #2422·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·

  ·

• Join: remove redundant universes from functor_join

  #2418·Alizter opened Oct 6, 2026Collaborator·

  ·

• Fix notation-level warnings

  #2417·Alizter opened Oct 6, 2026Collaborator·

  ·
  3

• Port developer compiler wrappers to Rocq

  #2415·Alizter opened Oct 6, 2026Collaborator·

  ·
  1

• Register dependent path rewriting

  #2414·Alizter opened Oct 6, 2026Collaborator·

  ·
  4

• Register existing elimination schemes

  #2413·Alizter opened Oct 6, 2026Collaborator·

  ·
  4

• Declare ordinary hint databases explicitly

  #2411·Alizter opened Oct 6, 2026Collaborator·

  ·
  3

• Construct the S3 H-space and clean up Cayley-Dickson

  #2409·Alizter opened Oct 5, 2026Collaborator·

  ·
  2

  

• Replace deprecated proof-ending tactics

  #2408·Alizter opened Oct 5, 2026Collaborator·

  ·
  2

• 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