| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares
|
|
|
|
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`.
|
|
|
|
|
|
|
|
For convenience
|
|
|
|
Reviewed-by: ejgallego
|
|
Otherwise gitlab stops logging somewhere in the middle.
Also pass -o because we can.
|
|
|
|
Reviewed-by: ejgallego
|
|
- don't `set -x` while loading overlays, non-verbose untaring
- ls _build_ci to help figure out artifact download issues
|
|
|
|
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
