All pull requests

Pull requests

• Replace and deprecate the aliased _env variants of Names sets and maps

  kind: cleanup
  #22542·ppedrot opened Sep 30, 2026Member·

  ·

  · 9.4+rc1

• Add additional extraction language in plugins

  #22541·vbergeron opened Sep 29, 2026·

  ·
  8

  

• Add a flag to disable the traversing subterm analysis

  needs: full CI
  #22540·thomas-lamiaux opened Sep 28, 2026Contributor·

  ·
  4

• [ssreflect] Accept tac; [tac|...|tac] => intro syntax

  kind: fixpart: ssreflect
  #22539·proux01 opened Sep 28, 2026Contributor·

  ·

  · 9.4+rc1
  1

  2

• Fix handling of polymorphic universes in ssr matching

  #22538·mattam82 opened Sep 26, 2026Member·

  ·
  5

• Turn Suggest Proof Using into a warning and add quickfix

  kind: enhancementkind: user messages
  #22532·SkySkimmer opened Sep 25, 2026Contributor·

  ·

  · 9.4+rc1
  5

• Add constant unfolding heuristic based on definitional heights.

  needs: full CI
  #22528·GPRicci opened Sep 24, 2026·

  ·
  6

• Do not use -unbox-closures

  kind: performance
  #22527·Janno opened Sep 24, 2026Contributor·

  ·
  8

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

• Notations: exclude only-printing declarations from prefix registration

  #22503·remix7531 opened Sep 17, 2026Contributor·

  ·
  1

  2

• Notations: allow only-printing level clashes

  #22502·remix7531 opened Sep 17, 2026Contributor·

  ·
  2

  1

• Optionally warn on admitted proofs

  kind: enhancementkind: user messagesneeds: changelog entry
  #22501·rlepigre-skylabs-ai opened Sep 17, 2026Contributor·

  ·

  · 9.4+rc1
  9

  

• Fix get_sigmatypes

  kind: internal
  #22499·mattam82 opened Sep 17, 2026Member·

  ·
  5

• Add a Scala 3 extraction backend

  needs: full CI
  #22487·vbergeron-ledger opened Sep 16, 2026·

  ·
  7

• Tactics: check for an interrupt between iterations of do

  needs: full CI
  #22485·remix7531 opened Sep 16, 2026Contributor·

  ·
  1

• rocqchk: fix soundness bug accepting proofs of False through forged delta aliases

  kind: inconsistency
  #22456·felix314159 opened Sep 9, 2026·

  ·
  3

  

• Add vm_compute_whnf and vm_compute_no_stuck

  needs: full CI
  #22441·Janno opened Sep 4, 2026Contributor·

  ·

• Speed up Search with a pattern for objects with very large types

  needs: full CI
  #22436·nbvdkamp opened Sep 2, 2026Contributor·

  ·
  6

• speed up Print Assumptions: walk stored proof term and exploit sharing

  needs: full CI
  #22425·zeldovich opened Aug 30, 2026Contributor·

  ·
  7

• kernel: conversion cache optimization experiment

  needs: rebasestale
  #22401·olympichek opened Aug 25, 2026Contributor·

  ·
  5

• Record the checks a module operation skipped

  kind: fixneeds: rebasepart: checkerpart: modules
  #22374·JasonGross opened Aug 19, 2026Member·

  ·
  2

  3

• kernel: store the conversion cache as flat integer arrays

  #22319·JasonGross opened Jul 28, 2026Member·

  ·
  3