Skip to content

Conversation

@ybertot
Copy link
Collaborator

@ybertot ybertot commented May 31, 2025

no more warning when executing rocq code for the tests
no more warning when compiling ml code (use of a threaded opaque_access instead of a Library.indirect_accessor)
Refreshed the documentation, including a suggestion from T. Bourke, and more compatible with the rocq renaming.

remove warnings
thread the opaque_access argument to avoid Library.indirect_accessor
@ybertot ybertot force-pushed the doc-n-warnings-May-25 branch from 66da48c to 96b1ddd Compare June 1, 2025 07:25
@ybertot ybertot requested a review from SkySkimmer June 2, 2025 07:02
@ybertot
Copy link
Collaborator Author

ybertot commented Jun 2, 2025

@SkySkimmer, can you please check that I used the "opaque_access" feature as you intended when you added the deprecation warning on Library.indirect_accessor

@ybertot ybertot merged commit 7817def into rocq-community:coq-master Jun 2, 2025
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants