Skip to content

Have implicit arguments with "Asymmetric Patterns"#21947

Merged
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
proux01:asymmetric-patterns-no-implicits
May 29, 2026
Merged

Have implicit arguments with "Asymmetric Patterns"#21947
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
proux01:asymmetric-patterns-no-implicits

Improve pattern externalization with Asymettric Patterns

0ff5c74
Select commit
Loading
Failed to load commit list.
coqbot-app / GitLab CI pipeline (pull request) succeeded May 28, 2026 in 1s

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