| Age | Commit message (Collapse) | Author |
|---|
|
As noted in GitHub discussion, it is a good idea to make `poly` always
explicit, this PR does remove last case of `?(poly=false)` in the
codebase.
|
|
Followup on "[api] Remove `polymorphic` type alias, use labels instead."
|
|
|
|
These are only needed when closing / admitting a proof.
|
|
|
|
|
|
This seems like the right location, a bit more refactoring should be
possible.
|
|
This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
|
|
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
|
|
This was already in the base proof object however not forwarded by
`close_proof`. thus it had to be stored twice.
There are more cases like this, like `poly`, all are covered by
subsequent commits.
|
|
|
|
Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
|
|
|
|
Information about interactive mutually recursive proofs was stored as
a closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
TODO: Should investigate what's going on with implicits, maybe submit
a separate PR.
|
|
Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
We prepare to put the information about rec_thms in the state too.
|
|
Reviewed-by: ejgallego
|
|
It was always the negation of the opacity flag.
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
|
|
|
|
Even more invariants can be enforced this way.
|
|
|
|
Mere isomorphism for now, but will allow more invariants ultimately.
|
|
This allows to desynchronize the kernel-facing API from the proof-facing one.
|
|
Nobody really knows where this module should belong, it seems. My personal
theory is that it should live in vernac instead, but due to nasty
interactions with abstract-like tactics, we have to put it somewhere below.
|
|
(fix #10350)
Ack-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
|
|
So far we didn't setup optimization flags for the VM in the Dune
build, but time has come to experiment with such flags, we try -O3.
Enabling `-flto` in the final binary build would be great, however
this seems to break windows.
|
|
Reviewed-by: Zimmi48
|
|
|
|
obligation ones.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
anomalies
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
|
|
|
|
in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
We place the check for unhandled exceptions in the `is_anomaly`
function, and consider all the exceptions non-handled by the printers
always anomalies.
This reworks the solution implemented in
ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular
`allow_uncaught` cannot be used anymore, all exceptions must install a
printer.
In order to pass the test-suite CI we also had to register some
printers, that were not registered for no reason, forcing clients to
call a post-processing step on errors.
|
|
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
|
|
|
