| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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`.
|
| |\
| |
| |
| | |
restructuration
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| | |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | | |
This was already the case, but the API was not exposing this.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| | | | | |
|
| | |/ / |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
| |\ \ \ |
|
| | | | | |
|
| |/ / /
| | |
| | |
| | |
| | |
| | | |
These functions were messing with the deferred universe constraints in an
error-prone way, and were only used for printing as of today. We inline
the one used by the printer instead.
|
| | |/
|/|
| |
| |
| | |
It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".
|
| | |
| |
| |
| |
| | |
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This string contains the base-10 representation of the number (big endian)
Note that some inner parsing stuff still uses bigints, see egramcoq.ml
|
| | | | |/
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.
We thus put the bullet functionality into its own, independent file.
|
| | | |/
| | |
| | |
| | |
| | |
| | | |
AFAICS this function predates modern state-handling; nowadays
summaries are stored by the STM and nobody were using this
information.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Matthieu Sozeau
Hugo Herbelin
Gaëtan Gilbert
Amin Timany
Matej Košík
Pierre Letouzey