| Age | Commit message (Collapse) | Author |
|---|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
|
sections
Reviewed-by: ppedrot
|
|
projections
Reviewed-by: fajb
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
|
|
universe unification
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
|
|
Reviewed-by: maximedenes
|
|
Should be 1:1 equivalent to the previous code, this is semantics preserving
factorization.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
No need to keep track of it this way now that this data is part of the
kernel.
|
|
This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.
As a nice bonus, this simplifies the Opaqueproof API.
|
|
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
|
|
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
|
|
This is not quite pretty, but it is needed by the section mechanism to rebuild
an inductive when closing a section. Hopefully this can be moved back at some
point.
|
|
For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
|
|
The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.
Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
intropattern entry in #10239)
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: fajb
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: mattam82
|
|
|
|
|
|
#10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Failing CI is BAD. #10476 should not have been merged without a
solution for SF being found, or the test being marked temporarily as
allow failure.
|
|
On tags, the pkg:nix:deploy:channel job was run even though the
required pkg:nix:deploy was not. We repeat the same conditions
regarding refs as in pkg:nix:deploy. Cf. GitLab's doc on the meaning
of several only conditions:
https://docs.gitlab.com/ee/ci/yaml/README.html#onlyexcept-advanced
|
|
It will take non-trivial effort to make Coq work with OCaml >= 4.10.0.
|
|
|
|
We allow the build to use some deprecated primitives in OCaml
4.09.0, for more details see bug #10602
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
