The Coq mailing list

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

Thanks Matthieu. That would definitely help a lot.

However, our comments sometimes also refer to definitions of earlier files.

Is there a way to get --interpolate to work even if the identifier was

declared in a different file that is included using Require Import/ Export?

Basically, coqdoc could issue a Locate command to coqtop 

for the identifier at the point it occurs in a comment

and use its output to determine the classification.

Does coqdoc already invoke coqtop?

-- Abhishek

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

On Tue, Jan 21, 2014 at 2:20 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

The --interpolate option will try to typeset the identifier with the most recent classification for it (in the same file), that's probably what you want.

Le lundi 20 janvier 2014, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

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/

--
-- Matthieu