# Developing the Rocq Prover

**URL:** https://discourse.rocq-prover.org/c/rocq-development/7.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [About the Developing the Rocq Prover category](https://discourse.rocq-prover.org/t/about-the-developing-the-rocq-prover-category/14)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [February 10, 2019, 9:47pm UTC](https://discourse.rocq-prover.org/t/about-the-developing-the-rocq-prover-category/14 "2019-02-10T21:47:25Z")

</div>

Use this category for any question or discussion related to the development of the Rocq Prover. This is the place to ask about how to contribute, to advertise RFCs, etc. Reporting bugs should be done on the bug tracker. …

---

## [Release of Rocq 9.3](https://discourse.rocq-prover.org/t/release-of-rocq-9-3/3064)

<div class="topic-metadata">

**Author:** [@gares](https://discourse.rocq-prover.org/u/gares)\
**Replies:** 0\
**Last updated:** [June 30, 2026, 8:57pm UTC](https://discourse.rocq-prover.org/t/release-of-rocq-9-3/3064 "2026-06-30T20:57:00Z")

</div>

Dear all, The branching date for the 9.3 release has been set to 2026-07-08. More details on the schedule are available here: Best, Your 9.3 Release Manager

---

## [Rocq 9.2 has just been scheduled](https://discourse.rocq-prover.org/t/rocq-9-2-has-just-been-scheduled/2883)

<div class="topic-metadata">

**Author:** [@nicolas\_tabareau](https://discourse.rocq-prover.org/u/nicolas_tabareau)\
**Replies:** 0\
**Last updated:** [December 17, 2025, 4:05pm UTC](https://discourse.rocq-prover.org/t/rocq-9-2-has-just-been-scheduled/2883 "2025-12-17T16:05:27Z")

</div>

Dear all, The branching date for the 9.2 release has been set to 2026-01-09. More details on the schedule are available here: \[ Release Schedule for Rocq 9.2 github.com \](https://github.com/rocq-prover…

---

## [Branch planning for 9.1](https://discourse.rocq-prover.org/t/branch-planning-for-9-1/2733)

<div class="topic-metadata">

**Author:** [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Replies:** 0\
**Last updated:** [June 6, 2025, 12:46pm UTC](https://discourse.rocq-prover.org/t/branch-planning-for-9-1/2733 "2025-06-06T12:46:21Z")

</div>

I plan to branch on 2025-06-11. If your PR milestoned for 9.1+rc1 is not expected to be ready by then please remove the milestone or set it to 9.1.0 (bugfix, user message and high priority changes) or 9.2+rc1. (Remove t…

---

## [What is the edit\_id or editId in the XML protocol?](https://discourse.rocq-prover.org/t/what-is-the-edit-id-or-editid-in-the-xml-protocol/2731)

<div class="topic-metadata">

**Author:** [@hehelego](https://discourse.rocq-prover.org/u/hehelego)\
**Replies:** 1\
**Last updated:** [June 6, 2025, 6:18am UTC](https://discourse.rocq-prover.org/t/what-is-the-edit-id-or-editid-in-the-xml-protocol/2731 "2025-06-06T06:18:19Z")

</div>

Hi all, I am looking into the coqidetop xml protocol and find the editId in the Add command quite confusing. Does anyone knows the intended meaning and how should XML protocol clients handle this id? FYI, an Add command…

---

## [Is there a public roadmap for the Rocq rename?](https://discourse.rocq-prover.org/t/is-there-a-public-roadmap-for-the-rocq-rename/2446)

<div class="topic-metadata">

**Author:** [@tchajed](https://discourse.rocq-prover.org/u/tchajed)\
**Replies:** 3\
**Last updated:** [October 11, 2024, 4:16pm UTC](https://discourse.rocq-prover.org/t/is-there-a-public-roadmap-for-the-rocq-rename/2446 "2024-10-11T16:16:03Z")

</div>

I saw that the next release after 8.20 is planned to be 9.0, and uses the name Rocq in the documentation. I’m wondering if there’s any public or private roadmap for this renaming. What I’m especially interested in is wh…

---

## [Why do we need supplemental standard libraries?](https://discourse.rocq-prover.org/t/why-do-we-need-supplemental-standard-libraries/2443)

<div class="topic-metadata">

**Author:** [@caverill](https://discourse.rocq-prover.org/u/caverill)\
**Replies:** 7\
**Last updated:** [October 7, 2024, 3:57pm UTC](https://discourse.rocq-prover.org/t/why-do-we-need-supplemental-standard-libraries/2443 "2024-10-07T15:57:31Z")

</div>

Why is Coq’s standard library “batteries not included”-style? I just saw this page for the first time, seeing the entire library represented so concisely is surprising: Standard Library | The Coq Proof Assistant. I’d cat…

---

## [I want Guidance on Extending Coq for Custom Proof Automation](https://discourse.rocq-prover.org/t/i-want-guidance-on-extending-coq-for-custom-proof-automation/2438)

<div class="topic-metadata">

**Author:** [@faelannm](https://discourse.rocq-prover.org/u/faelannm)\
**Replies:** 2\
**Last updated:** [September 28, 2024, 2:15am UTC](https://discourse.rocq-prover.org/t/i-want-guidance-on-extending-coq-for-custom-proof-automation/2438 "2024-09-28T02:15:04Z")

</div>

Hello All Member, I have been working with Coq for a few months now, mainly focusing on formal proofs in logic and set theory. I am interested in extending Coqs functionality for a specific project & want advice on how …

---

## [Idea for a collaborative Coq](https://discourse.rocq-prover.org/t/idea-for-a-collaborative-coq/2310)

<div class="topic-metadata">

**Author:** [@MrProof](https://discourse.rocq-prover.org/u/MrProof)\
**Replies:** 6\
**Last updated:** [June 1, 2024, 3:34pm UTC](https://discourse.rocq-prover.org/t/idea-for-a-collaborative-coq/2310 "2024-06-01T15:34:34Z")

</div>

Hi, I’m a software developer and I have an idea for a collaborate proof assistant using Coq that will help 100 mathematicians work on a proof at the same time. Here is my idea showing the various pages of the website: H…

---

## [8.20 branching next month](https://discourse.rocq-prover.org/t/8-20-branching-next-month/2291)

<div class="topic-metadata">

**Author:** [@proux01](https://discourse.rocq-prover.org/u/proux01)\
**Replies:** 0\
**Last updated:** [May 15, 2024, 9:32am UTC](https://discourse.rocq-prover.org/t/8-20-branching-next-month/2291 "2024-05-15T09:32:42Z")

</div>

Dear all, The branch for upcoming 8.20 is scheduled in about a month: please remove from the 8.20+rc1 milestone any pull request that you already know won't be ready by then.

---

## [Coq 8.19.0 tagged](https://discourse.rocq-prover.org/t/coq-8-19-0-tagged/2187)

<div class="topic-metadata">

**Author:** [@Gaetan\_Gilbert](https://discourse.rocq-prover.org/u/Gaetan_Gilbert)\
**Replies:** 0\
**Last updated:** [January 24, 2024, 12:48pm UTC](https://discourse.rocq-prover.org/t/coq-8-19-0-tagged/2187 "2024-01-24T12:48:01Z")

</div>

The tag is set to commit a360913fdc531715a33d06c29c4ff9fb8f1c3ac0.

---

## [Roadmap for Coq's source code and metatheory understanding.](https://discourse.rocq-prover.org/t/roadmap-for-coqs-source-code-and-metatheory-understanding/2172)

<div class="topic-metadata">

**Author:** [@qwertyuiop](https://discourse.rocq-prover.org/u/qwertyuiop)\
**Replies:** 1\
**Last updated:** [January 14, 2024, 7:43pm UTC](https://discourse.rocq-prover.org/t/roadmap-for-coqs-source-code-and-metatheory-understanding/2172 "2024-01-14T19:43:42Z")

</div>

What is the definitive roadmap to understanding Coq’s theory and source code for extremely skeptical and pedantic mathematician? Is there at least an order of reading sources? I want explicitly, not just be able to prove…

---

## [V8.19+rc1 tagged](https://discourse.rocq-prover.org/t/v8-19-rc1-tagged/2143)

<div class="topic-metadata">

**Author:** [@Gaetan\_Gilbert](https://discourse.rocq-prover.org/u/Gaetan_Gilbert)\
**Replies:** 0\
**Last updated:** [December 18, 2023, 4:29pm UTC](https://discourse.rocq-prover.org/t/v8-19-rc1-tagged/2143 "2023-12-18T16:29:11Z")

</div>

The release candidate has been tagged (Bump version to 8.19+rc1 · coq/coq@dba73c0 · GitHub). The final release should have the same behaviour unless we find some serious bugs. Package managers please prepare a version …

---

## [Upcoming 8.19 branch](https://discourse.rocq-prover.org/t/upcoming-8-19-branch/2089)

<div class="topic-metadata">

**Author:** [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Replies:** 0\
**Last updated:** [October 31, 2023, 2:26pm UTC](https://discourse.rocq-prover.org/t/upcoming-8-19-branch/2089 "2023-10-31T14:26:28Z")

</div>

A branch for Coq 8.19 will be created and enter feature freeze on 2023-11-27. Pull requests other than bugfixes and documentation updates which are not merged to master before then will not be available in 8.19 barring …

---

## [Tag V8.18.0 is set](https://discourse.rocq-prover.org/t/tag-v8-18-0-is-set/2033)

<div class="topic-metadata">

**Author:** [@gares](https://discourse.rocq-prover.org/u/gares)\
**Replies:** 4\
**Last updated:** [October 11, 2023, 1:12pm UTC](https://discourse.rocq-prover.org/t/tag-v8-18-0-is-set/2033 "2023-10-11T13:12:56Z")

</div>

This is a gentle note for the maintainers of Coq packages out there that the tag for 8.18.0 is out. I'll work myself on the opam packaging. Best,

---

## [Coq manual build with dune](https://discourse.rocq-prover.org/t/coq-manual-build-with-dune/2059)

<div class="topic-metadata">

**Author:** [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Replies:** 3\
**Last updated:** [October 9, 2023, 5:43pm UTC](https://discourse.rocq-prover.org/t/coq-manual-build-with-dune/2059 "2023-10-09T17:43:00Z")

</div>

Sorry for the very naive question, I have not compiled Coq for some time. I have read INSTALL.md and dev/doc/build-system.dune.md, but I can’t I find an explanation for this: $ cd ~/coqdev $ git clone https://github.co…

---

## [Terms modulo α-conversion and substitution](https://discourse.rocq-prover.org/t/terms-modulo-conversion-and-substitution/1920)

<div class="topic-metadata">

**Author:** [@carnotweat](https://discourse.rocq-prover.org/u/carnotweat)\
**Replies:** 1\
**Last updated:** [March 30, 2023, 4:08am UTC](https://discourse.rocq-prover.org/t/terms-modulo-conversion-and-substitution/1920 "2023-03-30T04:08:31Z")

</div>

Can someone explain how ,Coq development does not treat terms modulo α-conversion, therefore the ,substitution a\[x ← b\] can capture variables. However, it is capture-avoiding if b is closed, and this suffices to define …

---

## [Coq 8.17.0 tag has been set](https://discourse.rocq-prover.org/t/coq-8-17-0-tag-has-been-set/1916)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [March 27, 2023, 6:44am UTC](https://discourse.rocq-prover.org/t/coq-8-17-0-tag-has-been-set/1916 "2023-03-27T06:44:38Z")

</div>

Dear Coq developers and maintainers of Coq packages, The tag for the Coq 8.17.0 release has been set. It is now time to prepare updates to Coq packages. Thanks! Théo Zimmermann, release manager for the 8.17 release

---

## [Coq 8.16.1 has been tagged](https://discourse.rocq-prover.org/t/coq-8-16-1-has-been-tagged/1843)

<div class="topic-metadata">

**Author:** [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Replies:** 0\
**Last updated:** [November 25, 2022, 12:18pm UTC](https://discourse.rocq-prover.org/t/coq-8-16-1-has-been-tagged/1843 "2022-11-25T12:18:45Z")

</div>

The V8.16.1 tag is now public! Package managers should now start work on upgrading their packages.

---

## [Branching v8.17 soon](https://discourse.rocq-prover.org/t/branching-v8-17-soon/1838)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [November 16, 2022, 5:16pm UTC](https://discourse.rocq-prover.org/t/branching-v8-17-soon/1838 "2022-11-16T17:16:27Z")

</div>

Hello Coq contributors and maintainers, We are going to create the v8.17 branch in preparation for Coq 8.17 in the next few days. The tentative schedule can be found here: We have not followed the usual process of an…

---

## [Coq 8.16.0 has been tagged](https://discourse.rocq-prover.org/t/coq-8-16-0-has-been-tagged/1784)

<div class="topic-metadata">

**Author:** [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Replies:** 0\
**Last updated:** [September 5, 2022, 11:51am UTC](https://discourse.rocq-prover.org/t/coq-8-16-0-has-been-tagged/1784 "2022-09-05T11:51:16Z")

</div>

The V8.16.0 tag is now public! Package managers should now start work on upgrading their packages.

---

## [Coq 8.16+rc1 has been tagged](https://discourse.rocq-prover.org/t/coq-8-16-rc1-has-been-tagged/1667)

<div class="topic-metadata">

**Author:** [@Pierre-Marie\_Pedrot](https://discourse.rocq-prover.org/u/Pierre-Marie_Pedrot)\
**Replies:** 0\
**Last updated:** [June 1, 2022, 8:43pm UTC](https://discourse.rocq-prover.org/t/coq-8-16-rc1-has-been-tagged/1667 "2022-06-01T20:43:45Z")

</div>

Dear package managers, the V8.16+rc1 tag is now public. Please start preparing the corresponding packages for the upcoming 8.16.0 release! Thanks, PMP

---

## [Coq 8.15.2 tagged](https://discourse.rocq-prover.org/t/coq-8-15-2-tagged/1666)

<div class="topic-metadata">

**Author:** [@Gaetan\_Gilbert](https://discourse.rocq-prover.org/u/Gaetan_Gilbert)\
**Replies:** 0\
**Last updated:** [May 31, 2022, 11:49am UTC](https://discourse.rocq-prover.org/t/coq-8-15-2-tagged/1666 "2022-05-31T11:49:24Z")

</div>

The tag for 8.15.2 has been set.

---

## [Coq Working Group June 2022](https://discourse.rocq-prover.org/t/coq-working-group-june-2022/1645)

<div class="topic-metadata">

**Author:** [@maximedenes](https://discourse.rocq-prover.org/u/maximedenes)\
**Replies:** 4\
**Last updated:** [May 11, 2022, 12:32pm UTC](https://discourse.rocq-prover.org/t/coq-working-group-june-2022/1645 "2022-05-11T12:32:51Z")

</div>

Hello there, We had agreed some time ago (during a Coq Call) to hold a two-day Coq Working Group in June, at Inria Sophia-Antipolis. Here’s the evento to pick the date: Répondre au sondage - Coq Working Group June 2022 …

---

## [8.15.1 tagged](https://discourse.rocq-prover.org/t/8-15-1-tagged/1606)

<div class="topic-metadata">

**Author:** [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Replies:** 0\
**Last updated:** [March 22, 2022, 4:27pm UTC](https://discourse.rocq-prover.org/t/8-15-1-tagged/1606 "2022-03-22T16:27:46Z")

</div>

The tag for 8.15.1 has been set.

---

## [Generalizing coercions to infer typeclass arguments](https://discourse.rocq-prover.org/t/generalizing-coercions-to-infer-typeclass-arguments/1241)

<div class="topic-metadata">

**Author:** [@charguer](https://discourse.rocq-prover.org/u/charguer)\
**Replies:** 7\
**Last updated:** [March 9, 2022, 12:25pm UTC](https://discourse.rocq-prover.org/t/generalizing-coercions-to-infer-typeclass-arguments/1241 "2022-03-09T12:25:35Z")

</div>

The following example, using inhabited types, motivates the potential interest for allowing coercions to leverage typeclass inference. I wonder if there would be obstacles to supporting it. Set Implicit Arguments. Clas…

---

## [V8.15.0 tag set](https://discourse.rocq-prover.org/t/v8-15-0-tag-set/1525)

<div class="topic-metadata">

**Author:** [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Replies:** 0\
**Last updated:** [January 13, 2022, 4:20pm UTC](https://discourse.rocq-prover.org/t/v8-15-0-tag-set/1525 "2022-01-13T16:20:56Z")

</div>

The tag has been set. Opam packages, docker tags and platform versions will now be prepared.

---

## [Coq 8.15 RC1](https://discourse.rocq-prover.org/t/coq-8-15-rc1/1503)

<div class="topic-metadata">

**Author:** [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Replies:** 0\
**Last updated:** [December 7, 2021, 1:51pm UTC](https://discourse.rocq-prover.org/t/coq-8-15-rc1/1503 "2021-12-07T13:51:53Z")

</div>

The tag for the 8.15 first release candidate has been set (V8.15+rc1). The 8.15 release will not have any more changes other than bug fixes with low compatibility impact. Package managers, please start preparing 8.15-c…

---

## [Coq 8.15 branch date](https://discourse.rocq-prover.org/t/coq-8-15-branch-date/1461)

<div class="topic-metadata">

**Author:** [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Replies:** 0\
**Last updated:** [October 14, 2021, 10:42am UTC](https://discourse.rocq-prover.org/t/coq-8-15-branch-date/1461 "2021-10-14T10:42:03Z")

</div>

A branch for Coq 8.15 will be created and enter feature freeze on 2021-11-15. Pull requests other than bugfixes and documentation updates which are not merged to master before then will not be available in 8.15 barring …

---

## [Enforcing that the parser and the documented syntax are in sync](https://discourse.rocq-prover.org/t/enforcing-that-the-parser-and-the-documented-syntax-are-in-sync/1385)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [July 16, 2021, 12:25pm UTC](https://discourse.rocq-prover.org/t/enforcing-that-the-parser-and-the-documented-syntax-are-in-sync/1385 "2021-07-16T12:25:33Z")

</div>

Dear Coq developers and contributors, We’ve recently merged PR https://github.com/coq/coq/pull/14245. This PR introduces a new requirement for PR authors, that will be checked in the linter. If your PR modifies the Coq…

[Next page](https://discourse.rocq-prover.org/c/rocq-development/7.md?page=1)