Backports 9.0 #20055
Draft
Backports 9.0 #20055
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
ppedrot
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
@coqbot run full ci |
coqbot-app
bot
added
the
needs: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
468bd58 to
8f35cff
Compare
coqbot-app
bot
removed
request: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
8f35cff to
609a3bd
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
609a3bd to
1b51fab
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
1b51fab to
d115535
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
d115535 to
5c8556d
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
5c8556d to
bc2b2e8
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
bc2b2e8 to
8b96a68
Compare
coqbot-app
bot
removed
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
8b96a68 to
b0adb4a
Compare
coqbot-app
bot
added
the
needs: full CI
…tions We could instead change it to add parentheses to applications but that would probably make seriously unreadable terms. (cherry picked from commit e712b6d)
…es not adding parens to applications
new example for bidirectionality hints in refmam Co-Authored-By: Jim Fehrle <[email protected]> Co-Authored-By: Pierre Rousselin <[email protected]> (cherry picked from commit c7f83f4)
(cherry picked from commit 88ca27f)
Close rocq-prover#20695 (cherry picked from commit eca29fa)
Co-authored-by: Pierre Rousselin <[email protected]> (cherry picked from commit 759850a)
Following ocaml/opam-repository#27613 (cherry picked from commit 4ff54cc)
This is to make it possible to refer to these list items in links (e.g. for rocq-prover#20450). (cherry picked from commit 9674ab6)
(cherry picked from commit 7808a16)
Co-authored-by: Gaëtan Gilbert <[email protected]> (cherry picked from commit 72a4039)
(cherry picked from commit 536a16a)
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 (cherry picked from commit a5e5123)
instead of hard coding it (cherry picked from commit a08b3af)
Co-authored-by: Théo Zimmermann <[email protected]> (cherry picked from commit 72d4ff1)
(cherry picked from commit fcfed21)
Adjust the CSS selectors of rocqdoc to be closer to the ones of rocqtop. (cherry picked from commit 1a7a153)
…newline in rocqdoc blocks.
… Sphinx. Fix rocq-prover#16956. Fix rocq-prover#20717. Co-authored-by: Clément Pit-Claudel <[email protected]> (cherry picked from commit 1d46348)
…ion lists in recent versions of Sphinx.
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
backports-9.0
branch
from
9a8dd78 to
be75a73
Compare
coqbot-app
bot
removed
the
request: full CI
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.
No description provided.