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

"Print Grammar foobar." regression #9681

Closed
SkySkimmer opened this issue Mar 1, 2019 · 1 comment · Fixed by #10061
Closed

"Print Grammar foobar." regression #9681

SkySkimmer opened this issue Mar 1, 2019 · 1 comment · Fixed by #10061
Labels
kind: regression Problems that were not present in previous versions. part: notations The notation system.
Milestone

Comments

@SkySkimmer
Copy link
Contributor

Print Grammar foobar.
(* 8.8: Error: Unknown or unprintable grammar entry.
master: succeeds with no output
8.9: not tested *)
@steffahn
Copy link
Contributor

steffahn commented Mar 2, 2019

8.9 no output either.

A bit annoying, since there's currently no way (that I know of) of inspecting a custom grammar entry. ^^

@Zimmi48 Zimmi48 added kind: regression Problems that were not present in previous versions. part: notations The notation system. labels May 8, 2019
@coqbot coqbot added this to the 8.10+beta1 milestone May 13, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: regression Problems that were not present in previous versions. part: notations The notation system.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants