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

Clean up some code, improve debug info in fleche #145

Merged
merged 1 commit into from
Jan 5, 2023
Merged

Clean up some code, improve debug info in fleche #145

merged 1 commit into from
Jan 5, 2023

Conversation

artagnon
Copy link
Collaborator

@artagnon artagnon commented Jan 3, 2023

No description provided.

Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

Instead of duplicate the find check at every place the approach in #141 is preferred.

@ejgallego
Copy link
Owner

Ok, you can rebase on top of #146

fleche/doc.ml Outdated Show resolved Hide resolved
fleche/memo.ml Outdated Show resolved Hide resolved
fleche/doc.ml Outdated Show resolved Hide resolved
fleche/doc.ml Outdated Show resolved Hide resolved
fleche/doc.ml Outdated Show resolved Hide resolved
@artagnon artagnon changed the title Never have coq-lsp throw an exception Clean up some code, improve debug info in fleche Jan 3, 2023
@artagnon
Copy link
Collaborator Author

artagnon commented Jan 3, 2023

All fixed.

@ejgallego ejgallego self-assigned this Jan 3, 2023
@ejgallego ejgallego added this to the 0.1.2 milestone Jan 3, 2023
Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

Thanks, rebased on top of #148 , the extra verbosity of print_file:true didn't work well in my setup.

@ejgallego ejgallego merged commit d0b1f16 into ejgallego:main Jan 5, 2023
ejgallego added a commit that referenced this pull request Jan 8, 2023
This is a start to handle Coq Internal errors better. Some changes
were already in different form in the first versions of #145

c.f. #91
ejgallego added a commit that referenced this pull request Jan 8, 2023
This is a start to handle Coq Internal errors better. Some changes
were already in different form in the first versions of #145

c.f. #91
@artagnon artagnon deleted the noexcept branch January 11, 2023 11:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Archived in project
Development

Successfully merging this pull request may close these issues.

None yet

2 participants