Skip to content

Have implicit arguments with "Asymmetric Patterns"#21947

Open
proux01 wants to merge 3 commits intorocq-prover:masterfrom
proux01:asymmetric-patterns-no-implicits
Open

Have implicit arguments with "Asymmetric Patterns"#21947
proux01 wants to merge 3 commits intorocq-prover:masterfrom
proux01:asymmetric-patterns-no-implicits

Conversation

@proux01
Copy link
Copy Markdown
Contributor

@proux01 proux01 commented Apr 23, 2026 •
edited
Loading

Fixes / closes #21769

To ease the transition to the new behavior, a new flag Asymmetric Patterns No Implicits (off by default) enables to retrieve the previous behavior.

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

Overlays (to be merged before the current PR)

All overlays are only setting the new Asymmetric Patterns No Implicits flag wherever Asymmetric Patterns was already set.

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 23, 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 Apr 23, 2026
@rocq-prover rocq-prover deleted a comment from coqbot-app Bot Apr 23, 2026
proux01 added a commit to rocq-community/coq-ext-lib that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947
e0b5c4d
proux01 added a commit to proux01/kami that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947
c1716eb
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 23, 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 Apr 23, 2026
@proux01 proux01 added kind: fix This fixes a bug or incorrect documentation. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc. labels Apr 23, 2026
proux01 added a commit to proux01/HoTT that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947
b87737e
proux01 added a commit to rocq-community/coq-ext-lib that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947
fb2b65d
proux01 added 2 commits April 23, 2026 15:10
@proux01
Have implicit arguments with "Asymmetric Patterns"
140b6f0 
Add a flag "Asymmetric Patterns No Implicits" (false by default) that
can be set to true to retrieve the previous behavior of "Asymmetric
Patterns" (needed for backward compat).
@proux01
Improve pattern externalization with Asymettric Patterns
91955da
proux01 added a commit to proux01/mathcomp that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947
5dc2329
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 23, 2026
@proux01 proux01 force-pushed the asymmetric-patterns-no-implicits branch from d2251c7 to 071a812 Compare April 23, 2026 13:13
@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 Apr 23, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 23, 2026
@proux01 proux01 force-pushed the asymmetric-patterns-no-implicits branch from 071a812 to fd3b165 Compare April 23, 2026 13:56
@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 Apr 23, 2026
This was referenced Apr 23, 2026
Merged
Merged
Merged
Open
Merged
Merged
proux01 added a commit to proux01/fiat-crypto that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947
327c6f9
This was referenced Apr 23, 2026
Merged
Merged
This was referenced Apr 23, 2026
Merged
Open
@proux01 proux01 marked this pull request as ready for review April 23, 2026 16:04
@proux01 proux01 requested review from a team as code owners April 23, 2026 16:04
@proux01 proux01 mentioned this pull request Apr 23, 2026
Open
tchajed added a commit to rocq-community/atbr that referenced this pull request Apr 23, 2026
@tchajed
Merge pull request #49 from rocq-community/rocq21947
1806f95 
Adapt to rocq-prover/rocq#21947
Alizter added a commit to HoTT/Coq-HoTT that referenced this pull request Apr 23, 2026
@Alizter
Merge pull request #2353 from proux01/rocq21947
9cee811 
Adapt to rocq-prover/rocq#21947
JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947 (#2312)
ece682c
JasonGross pushed a commit to mit-plv/fiat that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947 (#131)
39ab663
JasonGross pushed a commit to mit-plv/rewriter that referenced this pull request Apr 23, 2026
@proux01
Adapt to rocq-prover/rocq#21947 (#201)
58f50c4
JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Apr 24, 2026
@proux01
Adapt to rocq-prover/rocq#21947 (#2311)
d00cba0
SkySkimmer
SkySkimmer approved these changes Apr 28, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see overlays have #[warning="-unknown-option"], do they really have this warning as error? If not IMO we shouldn't locally override it.

@SkySkimmer SkySkimmer self-assigned this Apr 28, 2026
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Apr 28, 2026
SkySkimmer
SkySkimmer reviewed Apr 28, 2026
View reviewed changes
Comment thread doc/changelog/08-vernac-commands-and-options/21947-asymmetric-patterns-no-implicits-Changed.rst
@@ -0,0 +1,8 @@
- **Changed:**
the bahavior of the :flag:`Asymmetric Patterns` flag, which no
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer Apr 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
the bahavior of the :flag:`Asymmetric Patterns` flag, which no
the behavior of the :flag:`Asymmetric Patterns` flag, which no

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 28, 2026

I see overlays have #[warning="-unknown-option"], do they really have this warning as error?

In most cases (not all) probably not.

If not IMO we shouldn't locally override it.

I'm not sure. As a user I'd rather avoid having a spurious warning on older versions of Rocq. The warning may become non spurious if we ever remove the flag one day, but then we'd probably deprecate it before, so users would have a chance to see a warning anyway. No strong opinion though (other than for mathcomp were we actually check compilation without warning on last release so it's mandatory there).

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Apr 28, 2026

but then we'd probably deprecate it before

It's already deprecated in this PR no?

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 28, 2026

Right, so I'd say we are fine.

proux01 added a commit to rocq-community/aac-tactics that referenced this pull request Apr 28, 2026
@proux01
Merge pull request #164 from rocq-community/rocq21947
cadc48a 
Adapt to rocq-prover/rocq#21947
proux01 added a commit to rocq-community/coq-ext-lib that referenced this pull request Apr 28, 2026
@proux01
Adapt to rocq-prover/rocq#21947
ea9fc30
proux01 added a commit to proux01/mathcomp that referenced this pull request Apr 28, 2026
@proux01
Adapt to rocq-prover/rocq#21947
2667303
proux01 added a commit to rocq-community/coq-ext-lib that referenced this pull request Apr 28, 2026
@proux01
Merge pull request #162 from rocq-community/rocq21947
ddd03d2 
Adapt to rocq-prover/rocq#21947
samuelgruetter added a commit to mit-plv/kami that referenced this pull request Apr 28, 2026
@samuelgruetter
Merge pull request #47 from proux01/rocq21947
0438148 
Adapt to rocq-prover/rocq#21947
proux01 added a commit to rocq-prover/stdlib that referenced this pull request Apr 28, 2026
@proux01
Adapt to rocq-prover/rocq#21947
9b897ac
proux01 added a commit to rocq-prover/stdlib that referenced this pull request Apr 28, 2026
@proux01
Merge pull request #259 from proux01/rocq21947
1d2db65 
Adapt to rocq-prover/rocq#21947
damien-pous pushed a commit to damien-pous/relation-algebra that referenced this pull request Apr 28, 2026
@proux01 @damien-pous
Adapt to rocq-prover/rocq#21947
ba18468
proux01 added a commit to proux01/mathcomp that referenced this pull request Apr 30, 2026
@proux01
Adapt to rocq-prover/rocq#21947
82a9b5d
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 30, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels

kind: fix This fixes a bug or incorrect documentation. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: implicit arguments The implicit arguments mechanism, generalizable variables, etc.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

Asymmetric Patterns sometimes adds parameters instead of just removing them (doesn't handle implicit arguments correctly)

2 participants

@proux01 @SkySkimmer