The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

The coqdoc manual says:

Coq material is quoted between the delimiters [ and ]

Suppose I define an Inductive type

Inductive Void := .

When I generated the latex file using coqdoc, this occurrence of 

Void exported to latex as \coqdocinductive{Void} 

Hence it is colored correctly.

However, if I refer to it later in comments:

(**  [Void] denotes the false proposition *)

this occurrence gets exported to latex as \coqdocvar{Void}.

I was expecting it to be exported as \coqdocinductive{Void} to be consistent.

Am I doing something wrong?

Or it was supposed to work in this (inconsistent) way?

If so, why would one want to use this [] feature?

-- Abhishek

http://www.cs.cornell.edu/~aa755/