| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is required by Sphinx 8.0. See
https://github.com/sphinx-doc/sphinx/issues/4460.
|
|
|
|
|
|
`.. bibliography::` puts the bibliography on its own page with its own title in
LaTeX, but includes it inline without a title in HTML [1], so we need to
maintain two separate copies of zebibliography.rst
[1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
|
|
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
|
|
|
|
|
|
|
|
|
|
As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.
We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
|
|
|
|
arguments
|
|
make make-pretty-timed- after -> make make-pretty-timed-after (remove
space between - and after) (and reflow paragraph)
Fix spacing around :: in print-pretty-single-time-diff
Closes #8396
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This snippet on pattern matching got lost in the process of migrating to Sphynx.
|
|
This warning makes it much easier to stop relying on `Set Automatic
Coercions Import`. Tested with success on math-classes.
|
|
|
|
|
|
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.
Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.
Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.
cc: #7155
|
|
Numeral Notations are not well-supported inside functors. We now give a
proper error message rather than an anomaly when this occurs.
|
|
Aliases of global references can now be used in numeral notations
|
|
|
|
As per https://github.com/coq/coq/pull/8064#discussion_r209875616
I decided to make it a warning because it seems more flexible that way;
users to are flipping back and forth between option types and not option
types while designing won't have to update their `abstract after`
directives to do so, and users who don't want to allow this can make it an
actual error message.
|
|
Also make `Check S` no longer anomaly
Add a couple more test cases for numeral notations
Also add another possibly-confusing error message to the doc.
Respond to Hugo's doc request with Zimmi48's suggestion
From https://github.com/coq/coq/pull/8064/files#r204191608
|
|
Some of this code is cargo-culted or kludged to work.
As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter. In
this case, the function registration must be synchronized with the
document state, but the functions should not be marshelled / stored
in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
In this case, the registration must be synchronized, and the function
should be marshelled / stored in the .vo.
In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.
In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.
The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality. For
plugins, a simple string suffices, as long as the string does not clash
between different plugins. In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files. Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.
----
Some of this code is response to comments on the PR
----
Some code is to fix an issue that bignums revealed:
Both Int31 and bignums registered numeral notations in int31_scope. We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins. This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
|
|
|
|
|
|
This parsing/printing method for nat should be just as fast as
the previous dedicated code. Moreover, we could now parse large
literals as nat numbers, by leaving them in a half-abstract form
such as (Nat.of_uint 123456). This form is convertible to the
closed (S (S (S ...))) form, so it shouldn't be a big deal for
compatibility, except for if some Ltac stuff relies on (S ...) to be
present after parsing. Of course, forcing the computation of
a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
|
|
|
|
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
