| Age | Commit message (Collapse) | Author |
|---|
|
We set the minimum Sphinx version in conf.py to the one that we test
in our CI and the one that is documented in doc/README.md. Hopefully,
it will allow users with lower Sphinx verisons get better error
messages.
|
|
Ack-by: JasonGross
Reviewed-by: Zimmi48
|
|
Reviewed-by: gares
|
|
Ack-by: JasonGross
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
|
proper user-level typing error
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Reviewed-by: vbgl
|
|
Detected incidentally in "validate" check for #8893.
|
|
|
|
|
|
|
|
Move existing entries.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
as assumptions
Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
Reviewed-by: ejgallego
|
|
Fixes coq/coq#10062.
The implementation is rough, and does not deal with leading,
trailing, or doubled periods, but the same can be said of the current
handling of leading numbers or primes.
|
|
(Merge of the initial version with #9983 was broken)
|
|
|
|
Reviewed-by: herbelin
|
|
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
We add a fast path when generalizing over variables.
|
|
It was fairly easy, the plugin defined an argument that was only used in
a vernacular extension. Thus marking it as VERNAC was enough not to link
to Ltac.
|
|
Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com>
|
|
Copy change's variants in change_no_check, since supposedly they should all be
supported. But they haven't been tested, and my example fails.
|
|
Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235.
- Add a new section at the end
- Document change_no_check, and convert_concl_no_check, address review comments
|
|
Ack-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.
We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
The OPAM build has been broken it seems since almost the beginning as
OPAM doesn't substitute variables in the almost undocumented
`build-env` form.
Packages built this way worked as Coq used a different method to
locate `coqlib`, however the value for `coqlib` was incorrect.
We set instead the right prefix using an explicit configure call.
|
|
A module allowing the user to build a UsualDecidableTypeFull from a pair
of such, exactly analogous to the extant PairDecidableType and
PairUsualDecidableType modules.
Co-authored-by: Jean-Christophe Léchenet <eponier@via.ecp.fr>
|
|
We also update the plugin tutorial.
This was already tried [in the same exact way] in #8811, however the
bench time was not convincing then, but now things seem a bit better,
likely due to the removal of some extra normalization somewhere.
Some more changes from #8811 are still pending.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.
|
|
This was introduced by @herbelin in
817308ab59daa40bef09838cfc3d810863de0e46, appears to have been
made unnecessary again by herbelin in
4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6.
At this point it appears to be completely unused.
|
