The Coq mailing list

["Robert R. Schneck" <schneck AT Math.Berkeley.EDU>]

On Tue, 25 Feb 2003, Pierre Corbineau wrote:
> On Tue, Feb 25, 2003 at 04:38:39PM +0100, Romain Janvier wrote:
> > I want to write something like that in a tactic:
> > Tactic Definition tac:=
> > Match Context With
> > ...
> > |[id: (EX ?1| ?2)|-?3] -> Induction id
> > ...
>
> Use the pattern [id: (ex ? ? ?)|-?] instead.

Along these lines, I've often wanted some way to see the "primitive" form
of the various notational devices.  Suppose I forget that EX is ex, or
that ~ is not, or some such; if I wanted to send such a term to Check or
Print, or use it in a pattern like above, things are very difficult.
If there could be a command to print a term without using any of the
special pretty-printing rules, that could be helpful in such a situation.

Robert