Repository navigation
same html title for all files (stdlib doc) #195
Description
In the HTML documentation, the HTML title is the same for all files ("Rocq Standard Library"). This is not very informative and makes difficult to find a file in an HTML browser with various Coq files open in different tabs.
(copy of rocq-prover/rocq#2511 for stdlib)
Activity
SkySkimmer commentedon Jul 17, 2025
I guess we have to do some version-dependent handling if we want to use rocq-prover/rocq#20907 without producing bad titles on older rocq versions.
Durbatuluk1701 commentedon Dec 12, 2025
This would be quite nice to have.
The solution from rocq-prover/rocq#20907 is great, but it might be even nicer if we could put the most relevant info first and do something like
@@TITLE@@ - Rocq <Core | Standard> Library?Or maybe the fact that this is a library from Core or Stdlib should be implicit since the title will include either Corelib, Stdlib, or Ltac2 (which seems like it maybe shouldn't get Core Library as it currently does)?
So something like
Rocq: @@TITLE@@ Library?Really just trying to avoid having super wide tabs to see what they are relevant to: