The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there a way to figure out what a line of Coq code parses to, in terms of tokens?  For example, if I have [Notation "i ⁻¹" := (isomorphism_inverse i) (at level 10).], how do I figure out what the right set of printing directives to give to coqdoc is?  None of the following work:

(** printing i ⁻¹ %\ensuremath{i^{-1}}% #i^-1# *)

(** printing 'i ⁻¹' %\ensuremath{i^{-1}}% #i^-1# *)

(** printing "i ⁻¹" %\ensuremath{i^{-1}}% #i^-1# *)

(** printing ⁻¹ %\ensuremath{^{-1}}% #^-1# *)

(** printing '⁻¹' %\ensuremath{^{-1}}% #^-1# *)

(** printing '⁻' %\ensuremath{^{-}}% #^-# *)

(** printing '¹' %\ensuremath{^{1}}% #¹# *)

(** printing ⁻ %\ensuremath{^{-}}% #^-# *)

(** printing ¹ %\ensuremath{^{1}}% #¹# *)

Thanks.

-Jason