| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
| |/
|
|
|
|
|
|
|
| |
Together with #1122, this makes `VernacInstance` the only command in
the Coq codebase that cannot be statically determined to open a proof.
The reasoning for the commands moved to `VtSideff` is that
parser-altering commands should be always marked `VtNow`; the rest can
be usually marked as `VtLater`.
|
| |
|
|
|
|
|
|
|
|
| |
We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.
We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.
This is a preliminary step for the work on attributes.
|
| | |
|
| |
|
|
| |
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
|
| |
|
|
|
|
|
|
|
| |
We interpret meta-commands directly, instead of going by an
intermediate "classifier step".
The code could still use some further refactoring, in particular, the
`part_of_script` bit is a bit strange likely coming from some special
treatment of `VtMeta` in the `query` call, and should go away.
|
| |
|
|
|
|
|
|
|
|
| |
The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.
We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |\
| |
| |
| | |
top of the linking chain.
|
| | |
| |
| |
| |
| | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
| |/
|
|
| |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
| |
|
|
|
| |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| | |
|
| |
|
|
|
| |
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
| |
The command has been broken for 15 years. It is basically dead code.
Its former behavior can be mimicked with Set Printing Implicit. Show.
|
| |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Pierre-Marie Pédrot
Matthieu Sozeau
Amin Timany
Théo Zimmermann
Matej Kosik