9.1

List view

Prepare 9.1 release

Status: Merged (completed).

rocq-prover/stdlibnumber 234

#234 In rocq-prover/stdlib;

· by proux01 was closed on Feb 10, 2026

dune generate unsorted All.v

Status: Merged (completed).

rocq-prover/stdlibnumber 231

#231 In rocq-prover/stdlib;

· by SkySkimmer was closed on Feb 4, 2026

clean up component dependencies of lia

Status: Merged (completed).

rocq-prover/stdlibnumber 150

#150 In rocq-prover/stdlib;

· by andres-erbsen was closed on Jan 31, 2026

Adapt to https://github.com/rocq-prover/rocq/pull/21478

Status: Merged (completed).

rocq-prover/stdlibnumber 228

#228 In rocq-prover/stdlib;

· by proux01 was closed on Jan 27, 2026

[CI] Update

Status: Merged (completed).

rocq-prover/stdlibnumber 229

#229 In rocq-prover/stdlib;

· by proux01 was closed on Jan 27, 2026

Cleanup warnings

Status: Merged (completed).

rocq-prover/stdlibnumber 226

#226 In rocq-prover/stdlib;

· by SkySkimmer was closed on Nov 28, 2025

Add new tactic "ensatz" for proving polynomial equalities with existential quantifier

Status: Merged (completed).

rocq-prover/stdlibnumber 160

#160 In rocq-prover/stdlib;

· by lyonel2017 was closed on Nov 24, 2025

Move test of rocq#1844 back to main repo

Status: Merged (completed).

rocq-prover/stdlibnumber 224

#224 In rocq-prover/stdlib;

· by SkySkimmer was closed on Nov 24, 2025

Adapt to https://github.com/rocq-prover/rocq/pull/21126

Status: Merged (completed).

rocq-prover/stdlibnumber 222

#222 In rocq-prover/stdlib;

· by proux01 was closed on Nov 7, 2025

Adapt to rocq-prover/rocq#21241 (byte_rec not defined from byte_rect)

Status: Merged (completed).

rocq-prover/stdlibnumber 221

#221 In rocq-prover/stdlib;

· by SkySkimmer was closed on Oct 31, 2025

Delete "Fixpoint" output test after it moved back to core repo

Status: Merged (completed).

rocq-prover/stdlibnumber 220

#220 In rocq-prover/stdlib;

· by SkySkimmer was closed on Oct 30, 2025

Adapt to https://github.com/rocq-prover/rocq/pull/21159

Status: Merged (completed).

rocq-prover/stdlibnumber 211

#211 In rocq-prover/stdlib;

· by proux01 was closed on Oct 28, 2025

Update refman to rocqrst

Status: Merged (completed).

rocq-prover/stdlibnumber 218

#218 In rocq-prover/stdlib;

· by proux01 was closed on Oct 28, 2025

Weaken assumption of Diaconescu's theorem

Status: Merged (completed).

rocq-prover/stdlibnumber 214

#214 In rocq-prover/stdlib;

· by jeanas was closed on Oct 24, 2025

Fix changelog

Status: Merged (completed).

rocq-prover/stdlibnumber 216

#216 In rocq-prover/stdlib;

· by SkySkimmer was closed on Oct 22, 2025

Fix typo in Zmod

Status: Merged (completed).

rocq-prover/stdlibnumber 215

#215 In rocq-prover/stdlib;

· by miriampolzer was closed on Oct 22, 2025

Fix statement of Rmult_gt_reg_l in RIneq.v

Status: Merged (completed).

rocq-prover/stdlibnumber 213

#213 In rocq-prover/stdlib;

· by damiendoligez was closed on Oct 21, 2025

Adapt to https://github.com/rocq-prover/rocq/pull/21107

Status: Merged (completed).

rocq-prover/stdlibnumber 210

#210 In rocq-prover/stdlib;

· by proux01 was closed on Oct 3, 2025

Uint63 notation φ and Φ don't put pseudo application at level 0

Status: Merged (completed).

rocq-prover/stdlibnumber 209

#209 In rocq-prover/stdlib;

· by SkySkimmer was closed on Sep 25, 2025

Adapt to https://github.com/rocq-prover/rocq/pull/20816

Status: Merged (completed).

rocq-prover/stdlibnumber 208

#208 In rocq-prover/stdlib;

· by proux01 was closed on Sep 10, 2025

Adapt to rocq-prover/rocq#20957 (remove parentheses in output test)

Status: Merged (completed).

rocq-prover/stdlibnumber 204

#204 In rocq-prover/stdlib;

· by yannl35133 was closed on Sep 10, 2025

Adapt to https://github.com/rocq-prover/rocq/pull/20855

Status: Merged (completed).

rocq-prover/stdlibnumber 180

#180 In rocq-prover/stdlib;

· by proux01 was closed on Sep 9, 2025

Adapt to rocq-prover/rocq#20902 (induction checks the right scheme)

Status: Merged (completed).

rocq-prover/stdlibnumber 194

#194 In rocq-prover/stdlib;

· by SkySkimmer was closed on Sep 4, 2025

[CI] Fix dpdgraph-test

Status: Merged (completed).

rocq-prover/stdlibnumber 206

#206 In rocq-prover/stdlib;

· by proux01 was closed on Sep 3, 2025

[Makefile] Don't attempt to compile hidden files

Status: Merged (completed).

rocq-prover/stdlibnumber 205

#205 In rocq-prover/stdlib;

· by proux01 was closed on Sep 2, 2025