The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Hello,

I've put the coqdoc-generated version of a development online, and I now
want to link to some parts of it. Unfortunately, there is one link to an
inductive that does not work, probably because its name is "wf".

More precisely, in the development, I have:

--8<---------------cut here---------------start------------->8---
Inductive wf : process -> Prop :=
...
--8<---------------cut here---------------end--------------->8---

Looking at the generated html, I see that "wf" is treated as a keyword
and does not have a name anchor:

--8<---------------cut here---------------start------------->8---
<span class="id" type="keyword">Inductive</span> <span class="id" 
type="keyword">wf</span> : <a class="idref" 
href="HOC01Defs.html#process"><span class="id" 
type="inductive">process</span></a> -&gt; <span class="id" 
type="keyword">Prop</span> :=<br/>
--8<---------------cut here---------------end--------------->8---

Is there a way to tell coqdoc that wf is an identifier and not
a keyword?

Thanks,

Alan