Skip to content
New issue

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

#

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

Already on GitHub? # to your account

Jump to bottom

Fail should not suppress output. #819

Closed
gares opened this issue Jul 4, 2024 · 2 comments
Closed

Fail should not suppress output. #819

gares opened this issue Jul 4, 2024 · 2 comments
Labels
bug Something isn't working

Comments

@gares
Copy link
Member

gares commented Jul 4, 2024 

Check nat nat. (* error message displayed *)
Fail Check nat nat. (* no message displayed, while we are used to see the error message turned into an info one *)
@rtetley rtetley added the bug Something isn't working label Jul 5, 2024
@gares
Copy link
Member Author

gares commented Jul 23, 2024

https://github.com/coq/coq/blob/c0c8be2c4f575034ff23c7972393cdc324df2334/vernac/vernacinterp.ml#L41-L59

@rtetley rtetley mentioned this issue Jul 23, 2024
Merged
@rtetley
Copy link
Collaborator

rtetley commented Jul 24, 2024

Closed by #842

@rtetley rtetley closed this as completed Jul 24, 2024
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gares @rtetley