coqdoc -g omits "Declare Instance"

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2389
From: Yevgeniy Makarov <emakarov@gmail.com>
Reported version: trunk
CC: @herbelin

[coqbot]

Comment author: Yevgeniy Makarov <emakarov@gmail.com>

The following is a part of the Coq.Structures.Equalities library.

Module Type IsEq (Import E:Eq).
Declare Instance eq_equiv : Equivalence eq.
End IsEq.

However, the output of coqdoc -g (and, therefore, the generated HTML library listings) contain only

Module Type IsEq (Import E:Eq).
End IsEq.

I have trunk 13419.

[coqbot]

Comment author: @herbelin

Hi Evgeny, I fixed it (by adding explicitly Declare Instance as a command, r13440) but the fix is not robust since option -g removes all the commands that are not known explicit known from coqdoc, leading to permanent coqtop/coqdoc synchronisation problems. Thus I let the report open.

[coqbot]

Comment author: @Zimmi48

Hugo, what is the status of this? Is the bug still worth to be left open? If there is a general issue with coqdoc, maybe a new bug report explaining it would be more suited?

[coqbot]

Comment author: @herbelin

Hugo, what is the status of this?

The "Declare Instance" case is fixed (https://coq.inria.fr/distrib/current/stdlib/Coq.Structures.Equalities.html#IsEq).

Is the bug still worth to be left open? If
there is a general issue with coqdoc, maybe a new bug report explaining it
would be more suited?

Yes, maybe a new bug would be better. Maybe worth also to see if Yann can explain us his new almost finished but not fully finished coqtop-based coqdoc.

[SkySkimmer]

Yes, maybe a new bug would be better.

Let's close this one then.