| Age | Commit message (Collapse) | Author |
|---|
|
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
|
|
in refman.
|
|
|
|
|
|
Follow-up of #8987.
|
|
|
|
Also remove a few undocumented settings
|
|
Namely, it does not explicitly open a scope, but we remember that we
don't need the %type delimiter when in type position.
|
|
This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.
Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
|
|
Mostly courtesy of Jason Gross.
|
|
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
|
|
|
|
to fix all misuses.
|
|
|
|
And a few more Sphinx fixes in passing.
|
|
As per https://github.com/coq/coq/pull/8965#discussion_r237225852
|
|
As per https://github.com/coq/coq/pull/8965/files#r237225852
|
|
Users can now register string notations for custom inductives.
Much of the code and documentation was copied from numeral notations.
I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.
Some choices about proofs of the new `byte` type were made based on
efficiency. For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast. (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)
In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).
There is unfortunately a decent amount of code duplication between
numeral notations and string notations.
I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.
Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type. This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type. (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)
N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.
Closes #8853
|
|
|
|
|
|
This introduces the warning “not-a-class” in the “typeclasses” category.
|
|
|
|
|
|
Remove objects without body from most chapters.
The remaining problems are all in the SSReflect chapter.
|
|
|
|
|
|
|
|
|
|
|
|
This adds an optional [Subgraph] part to the Print Universes command,
eg [Print Universes Subgraph(i j)] to print only constraints related
to i and j (and Prop/Set).
|
|
|
|
|
|
|
|
This mostly fixes text that was italicized instead of teletyped. When
possible, tactic names have been made to point to their documentation.
Also, the date of the 8.9 release has been proactively changed to
November.
|
|
|
|
|
|
Adressed comments by Guillaume and Jason
Updated according to Zimmi48's input.
Better link to custom entries
Fix typesetting
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The `Undo` command is not reliable.
|
|
|
|
|
|
|
|
|
|
|
