Issues

• Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)

  rocq-prover/stdlib#315 · Filter by author hy7pc8gfmf-dotcom opened on Oct 9, 2026

• Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)

  rocq-prover/stdlib#312 · Filter by author hy7pc8gfmf-dotcom opened on Oct 6, 2026

• Maintaining NaryFunctions

  rocq-prover/stdlib#293 · Filter by author CharlesAverill opened on Jul 15, 2026

• QArith: Add more rounding modes to complement Qfloor and Qceiling

  rocq-prover/stdlib#283 · Filter by author RyanGlScott opened on Jul 3, 2026
  2

• Inconsistent OPAM packaging of rocq-stdlib

  rocq-prover/stdlib#256 · Filter by author xavierleroy opened on Apr 2, 2026
  4

• deprecating List.nth in favor of List.nth_default

  rocq-prover/stdlib#243 · Filter by author andres-erbsen opened on Mar 4, 2026

• Importing PeanoNat.Nat shadows eq definition

  rocq-prover/stdlib#242 · Filter by author Villetaneuse opened on Mar 2, 2026
  3

• Documentation could be automatically deployed

  rocq-prover/stdlib#241 · Filter by author proux01 opened on Feb 23, 2026

• Releasing? (Docker CI images do not support latest stdlib)

  rocq-prover/stdlib#230 · Filter by author andres-erbsen opened on Jan 28, 2026
  11

• Using dune when installing the package

  rocq-prover/stdlib#225 · Filter by author rlepigre-skylabs-ai opened on Nov 14, 2025
  2

• Regression: Importing ZArith leads to setoid_rewrite performance degradation

  rocq-prover/stdlib#200 · Filter by author Janno opened on Jul 23, 2025
  2

• same html title for all files (stdlib doc)

  rocq-prover/stdlib#195 · Filter by author SkySkimmer opened on Jul 17, 2025
  2

• Github CI anomaly zoo

  rocq-prover/stdlib#168 · Filter by author andres-erbsen opened on Jun 7, 2025
  4

• Design: connecting booleans to their meaning

  rocq-prover/stdlib#165 · Filter by author andres-erbsen opened on Jun 5, 2025

• GitHub CI queuing

  rocq-prover/stdlib#153 · Filter by author andres-erbsen opened on May 31, 2025
  10

• Require status checks to pass before merging (for auto-merge, no policy change)

  rocq-prover/stdlib#148 · Filter by author andres-erbsen opened on May 13, 2025
  3

• CI: is there a way to see CI-built HTML documentation for an unmerged PR?

  rocq-prover/stdlib#145 · Filter by author andres-erbsen opened on May 10, 2025
  1

• CI jobs should explicitly set the name field

  rocq-prover/stdlib#142 · Filter by author JasonGross opened on May 6, 2025

• "Cachix setup coq" failed on CI

  rocq-prover/stdlib#140 · Filter by author andres-erbsen opened on May 4, 2025

• NoDup_dec definition is opaque

  rocq-prover/stdlib#125 · Filter by author olympichek opened on Mar 31, 2025

• What is the merging policy for stdlib? (contributing.md is nonsense)

  rocq-prover/stdlib#116 · Filter by author SkySkimmer opened on Mar 3, 2025
  2

• Keep All.v in topological order

  rocq-prover/stdlib#106 · Filter by author proux01 opened on Feb 12, 2025
  1

• int64 equivalent for ExtrOcamlIntConv

  rocq-prover/stdlib#3 · Filter by author liyishuai opened on Dec 21, 2024

• stdlib exports conflicting notations

  rocq-prover/stdlib#4 · Filter by author andres-erbsen opened on Dec 20, 2024

• Confusing warning: Using Vector.t is known to be technically difficult

  rocq-prover/stdlib#5 · Filter by author cogumbreiro opened on Dec 7, 2024
  5