Skip to content

Make f (x:=e)%s parse as f (x:=e%s) instead of (f (x:=e))%s - #22357

Merged
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
SkySkimmer:arg-scope
Aug 21, 2026
Merged

Make f (x:=e)%s parse as f (x:=e%s) instead of (f (x:=e))%s#22357
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
SkySkimmer:arg-scope

Conversation

@SkySkimmer

@SkySkimmer SkySkimmer commented Aug 18, 2026 •
edited by proux01
Loading

Copy link
Copy Markdown
Contributor

This also makes it stop relying on level tolerance.

Fix #22324

Overlay (to be merged in sync with the current PR)

@SkySkimmer
SkySkimmer requested review from a team as code owners August 18, 2026 11:50
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 18, 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 Aug 18, 2026
@SkySkimmer SkySkimmer added needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. labels Aug 18, 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 Aug 18, 2026
@SkySkimmer SkySkimmer added the needs: fixing The proposed code change is broken. label Aug 18, 2026
@SkySkimmer

SkySkimmer commented Aug 18, 2026

Copy link
Copy Markdown
Contributor Author

looks like moving the % to a separate entry breaks compatibility when there is a notation using %, cf color failure.
Reduced:

Reserved Notation "x %" (at level 1).

Check 0%nat. (* master: accepted, PR: unknown interpretation for "_ %" (parsed as "(0 %) nat") *)

proux01
proux01 reviewed Aug 18, 2026
View reviewed changes
Comment thread parsing/g_constr.mlg Outdated
Comment thread doc/sphinx/language/core/assumptions.rst Outdated
@proux01 proux01 added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: fixing The proposed code change is broken. needs: changelog entry This should be documented in doc/changelog. labels Aug 20, 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 Aug 20, 2026
@SkySkimmer SkySkimmer added needs: test-suite update Test case should be added to / updated in the test-suite. needs: overlay This is breaking external developments we track in CI. labels Aug 20, 2026
@proux01 proux01 mentioned this pull request Aug 20, 2026
Merged
@SkySkimmer @proux01
Make f (x:=e)%s parse as f (x:=e%s) instead of (f (x:=e))%s
d597975 
This also makes it stop relying on level tolerance.

Fix rocq-prover#22324
@proux01 proux01 added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. needs: test-suite update Test case should be added to / updated in the test-suite. labels Aug 20, 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 Aug 20, 2026
@proux01

proux01 commented Aug 20, 2026

Copy link
Copy Markdown
Contributor

@SkySkimmer CI "green", if my "fix" seems acceptable to you, I'll merge

@SkySkimmer

SkySkimmer commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

seems fine

@proux01 proux01 self-assigned this Aug 21, 2026
@proux01 proux01 added kind: fix This fixes a bug or incorrect documentation. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc. labels Aug 21, 2026
@proux01 proux01 added this to the 9.3.0 milestone Aug 21, 2026
@proux01

proux01 commented Aug 21, 2026

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app

coqbot-app Bot commented Aug 21, 2026

Copy link
Copy Markdown
Contributor

@proux01: You can't merge the PR because it hasn't been approved yet.

@proux01

proux01 commented Aug 21, 2026

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit 8274fc1 into rocq-prover:master Aug 21, 2026
9 of 10 checks passed
@coqbot-app

coqbot-app Bot commented Aug 21, 2026

Copy link
Copy Markdown
Contributor

@proux01: Please take care of the following overlays:

  • 22357-SkySkimmer-arg-scope.sh

proux01 added a commit to rocq-community/rocq-lsp that referenced this pull request Aug 21, 2026
@proux01
Adapt to rocq-prover/rocq#22357
8fdc13f 
Adapt to rocq-prover/rocq#22357
proux01 added a commit to rocq-community/rocq-lsp that referenced this pull request Aug 21, 2026
@proux01
Merge pull request #1110 from proux01/rocq22357
c9ae1cc 
Adapt to rocq-prover/rocq#22357
@SkySkimmer
SkySkimmer deleted the arg-scope branch August 21, 2026 11:25
gares added a commit to gares/coq that referenced this pull request Aug 31, 2026
@gares
Backport PR rocq-prover#22357: Make f (x:=e)%s parse as `f (x:=e%s)…
565636b 
…` instead of `(f (x:=e))%s`
@gares

gares commented Sep 1, 2026

Copy link
Copy Markdown
Member

Backporting the overlay does not work, I guess it got entangled with another change in the parser, see #22316 job https://github.com/rocq-prover/rocq/pull/22316/checks?check_run_id=99841289058 . I think I will put this into 9.4

This was referenced Sep 1, 2026
Closed
Merged
proux01 added a commit to rocq-community/rocq-lsp that referenced this pull request Sep 1, 2026
@proux01
Revert "Adapt to rocq-prover/rocq#22357"
1991f19 
This reverts commit 8fdc13f.
proux01 added a commit to rocq-community/rocq-lsp that referenced this pull request Sep 1, 2026
@proux01
Adapt to rocq-prover/rocq#22357
2635f09 
Adapt to rocq-prover/rocq#22357
@proux01

proux01 commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

Indeed, there was a conflict with the rocq-lsp overlay for #22161 . I permuted them so that it is now possible to pin a working rocq-lsp commit. So if you just pin rocq-lsp as in 2cd27dd everything is fine.

gares added a commit to gares/coq that referenced this pull request Sep 18, 2026
@gares
Backport PR rocq-prover#22357: Make f (x:=e)%s parse as `f (x:=e%s)…
e59c154 
…` instead of `(f (x:=e))%s`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@proux01 proux01 proux01 approved these changes

Assignees

@proux01 proux01

Labels

kind: fix This fixes a bug or incorrect documentation. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc.

Projects

Release management
Status: ...

Milestone

9.3.0

Development

Successfully merging this pull request may close these issues.

Unexpected "level tolerance" warning when mixing scope and explicit implicit arguments

3 participants

@SkySkimmer @proux01 @gares