Add anchors in Corelib html index #20680
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is to make it possible to refer to these list items in links (e.g. for rocq-prover#20450).
Villetaneuse
added a commit
to Villetaneuse/coq
that referenced
this pull request
May 26, 2025
I don't think the average user cares about other tactics languages when browsing this part of the tutorial. Other tactics languages are already mentioned in the "Creating new tactics" part of the refman. Add a reference to the Ltac2 part of the Rocq website. Prerequisite: rocq-prover#20680 Fixes/closes: rocq-prover#20450
doc/corelib/index-list.html.template
Outdated
| <dt> <b>Init</b>: | ||
| <dt> <a id="Init"><b>Init</b></a>: |
There was a problem hiding this comment.
Shouldn't the id be on the dt tag instead? Using an a tag seems wrong to me, those are typically used for links (with a href attribute).
There was a problem hiding this comment.
You are probably right. Changed it.
There was a problem hiding this comment.
making it a link to itself could also be nice
the refman has a thing that appears on hover
but probably more complicated to implement
There was a problem hiding this comment.
What do you prefer, then?
4fb04dd to
7808a16
Compare
|
Is there an artifact showing the result? |
|
Thanks! Is it satisfactory enough in your opinion? |
SkySkimmer
reviewed
Jun 2, 2025
doc/corelib/index-list.html.template
Outdated
| @@ -9,7 +9,7 @@ through the <tt>Require Import</tt> command.</p> | |||
| <p>The core library is composed of the following subdirectories:</p> | |||
|
|
|||
| <dl> | |||
| <dt> <b>Init</b>: | |||
| <dt id="Init"> <b>Init</b>: | |||
There was a problem hiding this comment.
Suggested change
| <dt id="Init"> <b>Init</b>: | |
| <dt id="Init"> <a href="#Init"><b>Init</b></a>: |
There was a problem hiding this comment.
you should do the change for the other headings too
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
silene
reviewed
Jun 2, 2025
723b2d5 to
536a16a
Compare
|
Juste added a forgotten '#' somewhere. |
SkySkimmer
approved these changes
Jun 4, 2025
|
@coqbot merge now |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is to make it possible to refer to these list items in links (e.g. for #20450).
Not a web person, so there may be better ways to do it.