New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Decoupled `ImplItemKind.class_instance_to_doc()` #431

Merged

clarus merged 6 commits into main from gy@DecoupleImplItemToDoc

Dec 22, 2023

Collaborator

InfiniteEchoes commented Dec 21, 2023 •

edited

Loading

This PR:

Rewritten class_instance_to_doc to class_instance_to_coq
Changed repectively the functions where it occurs
Slightly modified make_and_detect_warnings.py in case the detection is not working

InfiniteEchoes added 6 commits

December 21, 2023 17:43


          Decoupled ImplItemKind.class_instance_to_doc

ff5fbd7


          Applied justname to further reduce code

bac3360


          Deleted comment

64ea8fc


          cargo fmt

b9faab2


          Update snapshot


          Fixed bug and updated python script

8490e0f

clarus merged commit 1e58da4 into main

1 check passed

clarus deleted the gy@DecoupleImplItemToDoc branch

December 22, 2023 13:36

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet