All pull requests

Pull requests

• Add example for as match pattern and document degenerate match compilation

  kind: documentation
  #22590·SkySkimmer opened Oct 15, 2026Contributor·

  ·

• Nicer error for incorrect Proof using

  kind: user messages
  #22589·SkySkimmer opened Oct 15, 2026Contributor·

  ·
  1

• [WIP] Internalize "if g then ..." as "if g :> bool then ..."

  #22586·proux01 opened Oct 15, 2026Contributor·1 of 4 tasks·

  ·

• Add syntax for absolute names

  needs: overlay
  #22585·SkySkimmer opened Oct 14, 2026Contributor·

  ·
  6

• define_evar_as_sort generate a flexible univ instead of rigid

  kind: enhancementpart: universes
  #22583·SkySkimmer opened Oct 14, 2026Contributor·

  ·
  4

• Warn when including module types into plain modules.

  kind: cleanup
  #22580·ppedrot opened Oct 12, 2026Member·

  ·

  · 9.4+rc1
  10

  

• Define prelude gcd without traversing subterm analysis

  #22579·thomas-lamiaux opened Oct 11, 2026Contributor·3 tasks done·

  ·
  2

• Replace Fix_F definitions to avoid traversing subterm analysis

  needs: full CI
  #22577·thomas-lamiaux opened Oct 10, 2026Contributor·

  ·
  15

• Keep CMorphism internals fully polymorphic.

  kind: fixkind: performance
  #22575·ppedrot opened Oct 9, 2026Member·

  ·

  · 9.4+rc1
  7

  

• Fix speculative subterm ownership in fixpoint guard checking

  #22573·thomas-lamiaux opened Oct 9, 2026Contributor·2 tasks done·

  ·
  1

  1

• Universes and variances

  needs: full CIneeds: rebase
  #22571·mattam82 opened Oct 8, 2026Member·6 tasks·

  ·
  1

• refman: clarify inductive types and elimination principles

  kind: documentationneeds: full CI
  #22563·thomas-lamiaux opened Oct 5, 2026Contributor·2 tasks done·

  ·
  16

• Add a flag to disable guard-checking reduction

  needs: full CI
  #22562·thomas-lamiaux opened Oct 5, 2026Contributor·3 tasks done·

  ·
  2

• Add a flag to disable beta-iota cut support

  needs: full CI
  #22560·thomas-lamiaux opened Oct 5, 2026Contributor·3 tasks done·

  ·

• [coercions] Disactivate by default the "ambiguous-paths" warning

  kind: performancepart: coercions
  #22559·proux01 opened Oct 5, 2026Contributor·3 of 6 tasks·

  ·

  · 9.4+rc1
  6

  

• Pack the parameters in a record in Constr.compare_head_gen_leq_with.

  kind: cleanupneeds: full CI
  #22554·ppedrot opened Oct 2, 2026Member·

  ·

  · 9.4+rc1
  11

  

• Avoid calling Esubst.el_shft with negative argument

  needs: fixing
  #22553·SkySkimmer opened Oct 2, 2026Contributor·

  ·
  9

• Basic Info printing for apply and derived tactics (constructor etc)

  kind: user messages
  #22549·SkySkimmer opened Oct 1, 2026Contributor·

  ·

  · 9.4+rc1
  2

  1

• Fix #22547 (scope annotations shouldn't close shallow scopes)

  kind: fixpart: notations
  #22548·proux01 opened Oct 1, 2026Contributor·2 of 5 tasks·

  ·

  · 9.4+rc1
  1

• Add a flag to disable the traversing subterm analysis

  kind: enhancementneeds: full CI
  #22540·thomas-lamiaux opened Sep 28, 2026Contributor·3 tasks done·

  ·

  · 9.4+rc1
  43

  

• Add constant unfolding heuristic based on definitional heights.

  kind: feature
  #22528·GPRicci opened Sep 24, 2026·4 tasks done·

  ·

  · 9.4+rc1
  20

  

• Experiment: parallel checking of opaque bodies in rocqchk using ocaml5 parallelism

  needs: full CI
  #22520·SkySkimmer opened Sep 23, 2026Contributor·

  ·
  11

• parallelism resistent newprofile

  needs: full CIneeds: newer ocaml
  #22518·SkySkimmer opened Sep 23, 2026Contributor·

  ·
  2

• Minimal guard

  needs: full CIneeds: progresspart: inductives
  #22517·yannl35133 opened Sep 23, 2026Contributor·

  ·

• Change printing of raw universes from Foo.123 to Foo:123

  kind: user messages
  #22509·SkySkimmer opened Sep 18, 2026Contributor·

  ·

  · 9.4+rc1
  3