Search results

Primitive array axioms should be univ poly

Status: Open.

#244 In rocq-prover/stdlib;

· SkySkimmer opened on Mar 4, 2026

deprecating List.nth in favor of List.nth_default

Status: Open.

#243 In rocq-prover/stdlib;

· andres-erbsen opened on Mar 4, 2026

Importing PeanoNat.Nat shadows eq definition

Status: Open.

#242 In rocq-prover/stdlib;

· Villetaneuse opened on Mar 2, 2026

Documentation could be automatically deployed

Status: Open.

#241 In rocq-prover/stdlib;

· proux01 opened on Feb 23, 2026

Using dune when installing the package

Status: Open.

#225 In rocq-prover/stdlib;

· rlepigre-skylabs-ai opened on Nov 14, 2025

Regression: Importing ZArith leads to setoid_rewrite performance degradation

Status: Open.

#200 In rocq-prover/stdlib;

· Janno opened on Jul 23, 2025

same html title for all files (stdlib doc)

Status: Open.

#195 In rocq-prover/stdlib;

· SkySkimmer opened on Jul 17, 2025

Github CI anomaly zoo

Status: Open.

#168 In rocq-prover/stdlib;

· andres-erbsen opened on Jun 7, 2025

Design: connecting booleans to their meaning

Status: Open.

#165 In rocq-prover/stdlib;

· andres-erbsen opened on Jun 5, 2025

GitHub CI queuing

Status: Open.

#153 In rocq-prover/stdlib;

· andres-erbsen opened on May 31, 2025

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

Status: Open.

#148 In rocq-prover/stdlib;

· andres-erbsen opened on May 13, 2025

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

Status: Open.

#145 In rocq-prover/stdlib;

· andres-erbsen opened on May 10, 2025