All pull requests

Pull requests

• Fix proof of False: compute uniform parameters of nested fixpoints in the right environment

  needs: full CI
  #22645·sjawhar opened Oct 27, 2026·2 tasks done·

  ·

• Print Assumptions: keep sharing when cooking opaque proofs of a section with an inductive

  needs: rebase
  #22644·sjawhar opened Oct 26, 2026·2 tasks done·

  ·

• Add unification universe levels ℓi, never declared in the kernel

  needs: full CI
  #22643·mattam82 opened Oct 26, 2026Member·1 of 3 tasks·

  ·
  2

• Add undocumented warnings to the refman

  kind: documentation
  #22642·SkySkimmer opened Oct 26, 2026Contributor·

  ·

• Fix OCaml extraction callbacks for recursive functions

  needs: full CI
  #22641·julesmt opened Oct 26, 2026·

  ·
  1

  

• Unfold type abbreviations when locating a fixpoint’s recursive argument.

  kind: fix
  #22638·rlepigre-skylabs-ai opened Oct 26, 2026Contributor·

  ·

  · 9.4+rc1
  1

  2

  

• ssr: replace universe state unions by set_ustate when extending

  kind: cleanupkind: performance
  #22636·mattam82 opened Oct 25, 2026Member·2 tasks·

  ·

  · 9.4+rc1
  16

  

• rocqchk: report per-statement proof support

  needs: full CI
  #22635·sjawhar opened Oct 25, 2026·4 tasks done·

  ·
  1

• ssr: only add the universes of the rule used by a multirule rewrite

  #22634·mattam82 opened Oct 25, 2026Member·2 of 3 tasks·

  ·
  7

• ssr: thread a single universe state through matching instead of unions

  #22633·mattam82 opened Oct 25, 2026Member·2 of 3 tasks·

  ·
  7

• Mention -boot in refman command flag list

  kind: documentation
  #22630·SkySkimmer opened Oct 23, 2026Contributor·

  ·
  1

• CI: add rocq-linux-process-semantics and rocq-read-file

  kind: enhancementneeds: discussionpart: CI
  #22629·JasonGross opened Oct 23, 2026Member·

  ·
  3

• Print Assumptions: add per-reference output

  needs: full CI
  #22628·symbiogenesis opened Oct 22, 2026Contributor·

  ·
  1

• In guard, only put lifts on first element of stack

  kind: performancepart: fixpoints
  #22625·yannl35133 opened Oct 22, 2026Contributor·

  ·
  11

• rocqchk accumulate axioms without "opacify" logic

  kind: fixpart: checker
  #22623·SkySkimmer opened Oct 22, 2026Contributor·

  ·

  · 9.4+rc1
  1

• Parsing of + in univ_annot and univ_name_list

  needs: full CI
  #22621·alex44119 opened Oct 22, 2026·4 tasks done·

  ·
  13

• zify: only traverse relevant terms

  needs: full CI
  #22617·Janno opened Oct 21, 2026Contributor·6 tasks·

  ·
  9

• checker: add opt-in -axiom-free exit status

  needs: full CI
  #22609·symbiogenesis opened Oct 20, 2026Contributor·2 tasks done·

  ·
  1

  2

• Add the Skip Qed Typecheck flag: skip the kernel typing of opaque proofs at Qed

  kind: featureneeds: full CI
  #22608·sjawhar opened Oct 19, 2026·

  ·

  · 9.4+rc1
  42

  

• rocqchk: check opaque proofs in parallel in forked worker processes (-j N)

  needs: full CI
  #22607·sjawhar opened Oct 19, 2026·

  ·
  3

• Stop iterating through libobjects for Search

  kind: cleanup
  #22603·SkySkimmer opened Oct 19, 2026Contributor·

  ·
  1

  

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

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

  ·
  5

• [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: overlayneeds: rebase
  #22585·SkySkimmer opened Oct 14, 2026Contributor·

  ·
  6

• Define prelude gcd without traversing subterm analysis

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

  ·
  2