Skip to content

Conversation

@proux01
Copy link
Collaborator

@proux01 proux01 commented Feb 9, 2024

Fixes #1157

@proux01
Copy link
Collaborator Author

proux01 commented Feb 9, 2024

I should still test that.

@proux01
Copy link
Collaborator Author

proux01 commented Feb 9, 2024

@affeldt-aist that's the thing we just discussed at the beginning of the meeting.

@proux01
Copy link
Collaborator Author

proux01 commented Feb 9, 2024

So, my bad, apparently I forgot to ask for the reexport of some hint in my review of the initial PR #1119 (c.f., first commit of the current PR) and contra was mostly broken. This seems to fix this; so @Tragicus @affeldt-aist feel free to merge at your discretion.

@proux01 proux01 marked this pull request as ready for review February 9, 2024 15:19
@affeldt-aist affeldt-aist merged commit 1596217 into math-comp:master Feb 9, 2024
@proux01 proux01 deleted the rm_canonical branch February 9, 2024 15:51
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.

Experiment with Export and categories in contra.v

2 participants