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.

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

Anomaly when disabling a previously unbound notation in a custom grammar #17782

Closed
charguer opened this issue Jun 29, 2023 · 1 comment · Fixed by #17891
Closed

Anomaly when disabling a previously unbound notation in a custom grammar #17782

charguer opened this issue Jun 29, 2023 · 1 comment · Fixed by #17891
Labels
kind: anomaly An uncaught exception has been raised. part: notations The notation system.
Milestone
8.19+rc1

Comments

@charguer
Copy link
Contributor

In Coq 8.17.

Declare Custom Entry trm.
Disable Notation "'foo' _"  (in custom trm).

gives Anomaly "Uncaught exception Not_found."

If no custom entry is involved, a proper error message is produced: Found no matching notation to enable or disable.

herbelin added a commit to herbelin/github-coq that referenced this issue Jul 26, 2023
@herbelin
Fixing coq#17782: Not_found to catch on non-existing custom notation …
ead0777 
…to disable.
@herbelin herbelin mentioned this issue Jul 26, 2023
Merged
2 tasks
@herbelin herbelin added part: notations The notation system. kind: anomaly An uncaught exception has been raised. labels Jul 26, 2023
@herbelin
Copy link
Member

Thanks for noticing. Fixed by #17891.

herbelin added a commit to herbelin/github-coq that referenced this issue Jul 26, 2023
@herbelin
Fixing coq#17782: Not_found to catch on non-existing custom notation …
5e94a04 
…to disable.
coqbot-app bot added a commit that referenced this issue Aug 2, 2023
@coqbot-app @proux01
Merge PR #17891: Fixes #17782: anomaly when trying to disable a non e…
cf41421 
…xisting custom notation

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>
@coqbot-app coqbot-app bot added this to the 8.18.0 milestone Aug 2, 2023
@Zimmi48 Zimmi48 modified the milestones: 8.18.0, 8.19+rc1 Oct 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: anomaly An uncaught exception has been raised. part: notations The notation system.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging a pull request may close this issue.

Fixes #17782: anomaly when trying to disable a non existing custom notation herbelin/github-coq
3 participants
@herbelin @Zimmi48 @charguer