Skip to content

GenConstr can intern directly to constr - #22106

Merged
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
SkySkimmer:intern-gen
Aug 26, 2026
Merged

GenConstr can intern directly to constr#22106
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
SkySkimmer:intern-gen

Remove the overlay.

9623c35
Select commit
Loading
Failed to load commit list.
coqbot-app / GitLab CI pipeline (pull request) succeeded Aug 26, 2026 in 0s

Full pipeline completed successfully on GitLab CI

This GitLab pipeline sets the following variables:

  • FULL_CI: true

It contains the following stages and jobs:

GitLab Project ID: 4504