| Age | Commit message (Collapse) | Author |
|---|
|
We re-expose `declare_projections` and `declare_structure_entry` as it
is needed by coq-elpi.
Ideally we would provide a better way in recordops to interact with
this, in fact `declare_structure_entry` is just a wrapper around
recordops + libobject structure so there is hope it goes away entirely
in the future.
The need for Elpi to manually call `declare_projections` should
actually disappear in future refactorings.
|
|
Also add nice error message when the grep produces an empty result
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
Git wants an identity and none is setup on the CI.
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares
|
|
This avoids the need to rebase the overlay when nothing has changed.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
|
|
|
|
|
|
a context.
Reviewed-by: mattam82
|
|
|
|
Also pass `--output-sync` on the CI, as suggested in
https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect
against this failure mode.
Fixes #13062
|
|
After #8743 we don't depend on `num` anymore in the codebase; thus we
drop the dependency.
This could create problems for plugins relying on this implicit
linking.
|
|
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in
1.10, see
https://github.com/ocaml/Zarith/issues/58
|
|
- `odoc` must be bumped to support 4.11
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
- take just a ugraph instead of the whole env
- rename to update_sigma_univs
- push global env lookup a bit further up
- fix vernacinterp call to update all surrounding proofs, not just the
top one
- flip argument order for nicer partial applications
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
|
|
Reviewed-by: ejgallego
|
|
Tests moved in https://github.com/whonore/Coqtail/pull/134.
|
|
Added user overlay for bignums
|
|
recognition.
Reviewed-by: mattam82
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
|
|
|
