Skip to content

Add "& T" syntax for anonymous binder "(_ : T)" and "of _ & _ & _" syntax for constructors#21611

Merged
coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom
proux01:of-ampersand
Feb 26, 2026
Merged

Add "& T" syntax for anonymous binder "(_ : T)" and "of _ & _ & _" syntax for constructors#21611
coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom
proux01:of-ampersand

Commits

Commits on Feb 26, 2026