The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

On Wed, Nov 18, 2015 at 09:14:22AM -0800, Michael Shulman wrote:
> Is there a command to display the level of a particular notation?

I don't think so.

> So far the only ways I have found to figure out the level of a
> notation are to try to track down the source file where the notation
> was declared, or to "Print Grammar constr" and search through the (not
> very user-friendly) output for the notation in question.

I think so.

> "Locate" shows what a notation is defined to mean, but not its level.

Indeed, Locate could also show the level. Here are entry points if
ever someone is willing to submit such a refinement of Locate as a
pull request: in source code, looking at Notation.locate_notation;
parsing/printing data including level should be obtainable from
Notation.find_notation_printing_rule.

Best,

Hugo