| Age | Commit message (Collapse) | Author |
|---|
|
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line.
The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed,
then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
|
|
|
|
|
|
We use a more robust implementation that does not assume that the type
of the inductive is in ζ-normal form. This code path is not exercised,
because due to the kernel typing algorithm, let-bindings in the type
of a recursor are expanded away.
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
|
|
Reviewed-by: Matafou
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: jfehrle
|
|
We include the `version=0.13.0` field that should help users not to
use the wrong version. `disable=true` still seems a noop with `dune`.
There are some minor changes in the way comments are formatted; I'm
unsure if this is due to the `wrap-comments` option; as always; tweaks
to the config are most welcome.
|
|
There is a lot of check overhead in the code, we will try to provide a
more convenient API for manipulation of remaining obligations.
|
|
Both the interactive and non-interactive save path share some internal
table update code.
|
|
We make internal types `private` as an step towards the unification of
the save path with the rest of the system.
In particular, this is allow us to guarantee invariants
w.r.t. external users as the large majority of fields are always
constant.
This will also enable at some point a common creation of proof entry
with the rest of the system.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
After we moved `start_lemma_com` to `vernacentries` the comment on
`start_lemma_with_initialization` needs update.
|
|
It should be safe now after previous refactoring in lemmas.
|
|
This is a step towards cleanup of the `start` lemma path.
|
|
|
|
We instead favor the `build_by_tactic` function which should at some
point better integrated in the declare core.
|
|
In anticipation for more consolidation of duplicated functionality.
|
|
Most of the parameters were named, we fix the remaining cases.
|
|
fixed bug
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.
|
|
following changes to attribute parsing.
|
|
And fix documentation following the removal of the Template Check flag
in #11546.
|
|
- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).
We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
|
|
As a first step toward a deeper refactoring of the reference manual,
we move existing chapters into a new structure.
We use the Sphinx support for top-level chapters spanning multiple
pages to consolidate existing chapters into a smaller number of
chapters and a smaller number of parts.
Now the full top-level table of content can be seen in one glance.
Most of the new chapters are divided into several sub-chapters (on
separate pages) that correspond to the pre-existing chapters. These
new top-level chapters gathering several chapters together have gained
a new introduction. The main introduction has been rewritten /
simplified as well.
For now, the URL of pre-existing chapters does not change. The intent
is to further refactor the manual by splitting some of these
sub-chapters into smaller ones, and by moving things around.
While the sub-chapters are likely to evolve very much in the future,
the top-level table of content is almost final (except that the "Using
Coq" part may gain one or two additional chapters on proof engineering
/ project management).
Thanks to Jim Fehrle for investigating how to split a chapter on
multiple pages and to both Jim and Matthieu Sozeau for the discussion
that led to this new structure.
See also the related CEP: https://github.com/coq/ceps/pull/43
Additional notes:
- A new directory structure has been created reflecting the new
chapter structure.
- The indexes chapter has been removed from the PDF version since it
wasn't working.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Ack-by: herbelin
|
|
Reviewed-by: JasonGross
Reviewed-by: ppedrot
|
|
|
|
This enforces monomorphism everywhere possible.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
