| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
|
|
|
|
Reviewed-by: gares
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
After #12023 broke the bug minimizer, I'd like to add
[coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's
relatively light-weight (under 5 minutes, I believe), and I'd like to
know when it's going to break on master before it's broken, rather than
after. It tests a relatively under-tested part of Coq, mostly (the
display output of error message, by and large), and I'm happy to take
responsibility for fixing it when some PR is going to break it (mainly I
just want a sort-of early warning system, and I want PRs to not
accidentally break it by changing things that they don't realize they're
changing).
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
Indeed, it would be intuitive that `Require Import Ltac` is an
equivalent for Ltac of `Require Import Ltac2.Ltac2`.
Also declaring the classic proof mode.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
|
|
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
No diff to sources (luckily), see release notes at
https://discuss.ocaml.org/t/ann-ocamlformat-0-14-0/5435 for more
information.
|
|
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0
|
|
Cf. #12049.
|
|
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
|
|
Auto-generated files like the Makefile have recently been removed from
the sources (cf. coq-community/corn#88). Calling ./configure.sh is
now required.
|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: ejgallego
|
|
Ack-by: Matafou
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
- problem with metacoq overlay ; it expects to send a non-ground
constant to the kernel, now it fails at prepare.
Record Sigma (A : Type) (B : A -> Type) : Type :=
{ fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.
Quote Recursively Definition foo := (fst, snd).
There is a hack on the overlay, we need to discuss it a bit more.
|
|
Fix #11967
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
I believe a recent commit to master broke it, and now that it's no
longer tested as part of fiat-crypto-legacy, I think it's time to add
it.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but
only the non-ignored files will be affected.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
