Skip to content

Deprecate non boolean if syntax#22123

Draft
proux01 wants to merge 3 commits into
rocq-prover:masterfrom
proux01:deprecate-if
Draft

Deprecate non boolean if syntax#22123
proux01 wants to merge 3 commits into
rocq-prover:masterfrom
proux01:deprecate-if

Conversation

@proux01

@proux01 proux01 commented Jun 12, 2026

Copy link
Copy Markdown
Contributor

Deprecate the non boolean if t then _ else _ syntax (in favour of if t is <first_constructor> then _ else _).

Depends on: #21609

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
    • Updated documented syntax by running make doc_gram_rsts.

@proux01 proux01 added needs: merge of dependency This PR depends on another PR being merged first. kind: deprecation Deprecation labels Jun 12, 2026
@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 12, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 12, 2026
@coqbot-app coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jun 12, 2026
@proux01 proux01 added this to the 9.3+rc1 milestone Jun 12, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 12, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 12, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

Is printing of non booleans changed to use the new syntax too?

@proux01

proux01 commented Jun 12, 2026

Copy link
Copy Markdown
Contributor Author

I'm working on it (in a separate PR)

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: deprecation Deprecation needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: merge of dependency This PR depends on another PR being merged first.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants