Janno/test 21247#2

Draft

Janno wants to merge 151 commits into

skylabs-masterfrom

janno/test-21247

Commits on Jun 12, 2025

Pin CI for 9.1
SkySkimmer
committed

Commits on Jun 13, 2025

Commits on Jun 16, 2025

Commits on Jun 17, 2025

Commits on Jun 18, 2025

Commits on Jun 19, 2025

Fix #20679: avoid spurious newline in rocqdoc blocks.

Zimmi48
authored and
SkySkimmer
committed
Backport PR #20710: Fix #20679: avoid spurious newline in rocqdoc blocks.
SkySkimmer
committed
Fix level of Ltac1CompatNotations transitivity notation
SkySkimmer
committed
Backport PR #20758: Fix level of Ltac1CompatNotations transitivity notation
SkySkimmer
committed
Update coqdev email in dune-project
SkySkimmer
committed
Backport PR #20768: Update coqdev email in dune-project
SkySkimmer
committed
Record fields can have decl_notations

Villetaneuse
authored and
SkySkimmer
committed
Example of where clause in record field in refman

Villetaneuse
authored and
SkySkimmer
committed
Document where clause in the record_field part

Villetaneuse
authored and
SkySkimmer
committed
Small rewording in record field where clause exple

Villetaneuse
authored and
SkySkimmer
committed
Update doc/sphinx/language/core/records.rst

authored and
SkySkimmer
committed
Move descr to match order of gram in records.rst

Villetaneuse
authored and
SkySkimmer
committed
Backport PR #20753: Document where clauses in record fields
SkySkimmer
committed
Fix broken links in refman

ia0
authored and
SkySkimmer
committed
Backport PR #20773: Fix broken links in refman
SkySkimmer
committed

Commits on Jun 24, 2025

Commits on Jun 25, 2025

Commits on Jun 30, 2025

Commits on Jul 1, 2025

Commits on Jul 2, 2025

Commits on Jul 3, 2025

Commits on Jul 4, 2025

bump coq-elpi and metarocq pins
gares
committed

Commits on Jul 7, 2025

Commits on Jul 8, 2025

Commits on Sep 3, 2025

Commits on Sep 5, 2025

Commits on Sep 15, 2025

Final commit for 9.1.0
SkySkimmer
committed

Commits on Sep 17, 2025

[BR] Add FM CI setup.

Rodolphe Lepigre
authored and
Jan-Oliver Kaiser
committed
[BR] Enable native dune rules.

Rodolphe Lepigre
authored and
Jan-Oliver Kaiser
committed
[BR] disable documentation and test suite build.

Rodolphe Lepigre
authored and
Jan-Oliver Kaiser
committed
Omit coqide from dune-project WIP

Blaisorblade
authored and
Jan-Oliver Kaiser
committed
Empty coqide package

Blaisorblade
authored and
Jan-Oliver Kaiser
committed
Drop coqide_gui library to drop gtk dependency

Blaisorblade
authored and
Jan-Oliver Kaiser
committed
[BR] Move coqc/coqdep into rocq-core to enable composed builds

Blaisorblade
authored and
Jan-Oliver Kaiser
committed
[BR] Add br_timing profile

Blaisorblade
authored and
Jan-Oliver Kaiser
committed
Fix rocq-test-suite package
Jan-Oliver Kaiser
committed
[BR] Cherry-picked: Remove dev/shim

SkySkimmer
authored and
Jan-Oliver Kaiser
committed

Commits on Oct 14, 2025

[BR/SL integration] adapt CI config.

rlepigre-skylabs-ai
authored and
Janno
committed

Commits on Oct 29, 2025

Commits on Nov 4, 2025

Bake the NonLogical run in Logic_monad.run.

ppedrot
authored and
Janno
committed
Collapse NonLogical thunks in the logic monad.

ppedrot
authored and
Janno
committed