Skip to content
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.

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

Rename McLTT modules into McTT #260

Closed
Ailrun opened this issue Nov 8, 2024 · 6 comments · Fixed by #266
Closed

Rename McLTT modules into McTT #260

Ailrun opened this issue Nov 8, 2024 · 6 comments · Fixed by #266

Comments

@Ailrun
Copy link
Member

Ailrun commented Nov 8, 2024

Although the repo itself is renamed, there are some leftover "McLTT"s in this codebase.
They should be renamed.

@HuStmpHrrr
Copy link
Member

also remember to change the hintdb to mctt as well.

@Ailrun
Copy link
Member Author

Ailrun commented Nov 16, 2024

#262 changed the main branch. Now we need to port the change into ext/prop-eq branch (which is probably even less complex, as infra-related changes are all done in that PR).

@HuStmpHrrr
Copy link
Member

A merge will handle almost everything, no?

@HuStmpHrrr
Copy link
Member

McTT/theories/Makefile

Lines 46 to 47 in 2f662c9

update_CoqProject: clean
(echo "-R . Mcltt"; \

leftover

What is this? is it still needed?

@Ailrun
Copy link
Member Author

Ailrun commented Nov 16, 2024

@HuStmpHrrr Oh, yes. That's a helper target (which generates _CoqProject automatically). I will update that one as well.

@Ailrun Ailrun mentioned this issue Nov 16, 2024
@Ailrun
Copy link
Member Author

Ailrun commented Nov 16, 2024

@HuStmpHrrr
A merge will handle almost everything, no?

For example, _CoqProject added some modules, so we need to change them to use Mctt.

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 a pull request may close this issue.

2 participants