| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: herbelin
Ack-by: jfehrle
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: cpitclaudel
|
|
And also clean INSTALL file of useless reminder of the procedure to
install using a package manager.
|
|
|
|
the kernel
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
main path
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.
Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.
|
|
All section definitions are always defined as if they were transparent,
all the additional checks were actually never triggered.
|
|
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
We turn the hook parameter into a record, making more explicit the
capture of data in hooks as they only take one parameter now
This is a fine-tuning but provides some small advantages, and allows
us to tweak the hook type with less breakage.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
It prints a goal given its internal goal id and the Stm state id.
|
|
Ack-by: Zimmi48
Reviewed-by: gares
|
|
We move the stack of open lemmas from `Lemmas` to `Vernacstate`. The
`Lemmas` module doesn't deal with stacked proofs, so the stack can be
moved to to the proper place; this reduces the size of the API.
Note that `Lemmas` API is still quite imperative, it would be great if
we would return some more information on close proof, for example
about the global environment parts that were modified.
|
|
It is completely local to that file, there was no point to put it into
the unrelated Declare file.
|
|
It was never used actually.
|
|
|
|
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
|
|
|
|
|
|
theorems.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
with coqtop
Reviewed-by: gares
Ack-by: jfehrle
|
|
Reviewed-by: vbgl
|
|
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.
|
|
|
