| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We do not partially abstract the section info. Instead, we reuse the same
code in cook_constr and cook_constant and pass the same section info.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Cooking
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: gares
|
|
Ack-by: RalfJung
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes
|
|
We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.
The list is provisional and should be subject to change, let's see
what CI says.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
|
|
They are supposed to be included in the module's constraints.
The old behaviour would allow a crafted vo, using
~~~coq
Definition a := Type.
Definition b := Type.
Definition b_in_a : a := b.
Definition a_in_b : b := a.
~~~
with the constraints for b_in_a and a_in_b not included in the module
constraints, then a proof of false may be derived in the usual way.
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
We crawl the context in the other direction, preventing the allocation of
the return boolean and enhancing sharing. This fast-path is assuming the
heuristic that the variable being renamed always appears in the context,
otherwise we would be renaming for nothing. It seems to always be the
case, due to the way we pick the set of names to be avoided.
|
|
Instead of blindly renaming the variables in all the terms in the context,
we only do so for those appearing after the variable being renamed. By
typing, we know that the other ones cannot refer to the variable being
replaced.
Fixes #9992.
|
|
|
|
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
|
|
Reviewed-by: gares
Ack-by: maximedenes
|
|
We use the right environment.
|
|
For now this is just a specialized version of the previous generic code.
This simplifies tracking of the changes.
|
|
It is guaranteed by Declare, but a little dynamic check does not hurt.
|
|
The only lawbreaker was the Add Ring command. We generate a type for
the declaration to fix the code.
|
|
The idea is that it's unlikely for only 1 of the test suite copies to
fail for a real reason, so we don't need to run all of them.
I would prefer to have only 1 build stage job but later stages depend
on build:base, build:edge+flambda and build:edge+flambda:dune:dev for
non-copy-pasted jobs.
I kept corresponding test suite and validate job copies but they could
also be filtered.
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: gares
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
|
|
This is the intended module for the feature provided by the inductive
discharge. This allows for a bit of code sharing and cleanup.
|
|
|
|
|
|
options rather than files
Reviewed-by: ejgallego
|
|
patn]".
Reviewed-by: Zimmi48
|
|
than files.
|
|
sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
|
|
Safe_typing is now responsible for hashconsing of all accessible structures,
except for opaque terms which are handled by Opaqueproof.
|
|
A link to this file will be displayed when people start opening an
issue, and maybe in some other places.
See also:
https://help.github.com/en/articles/adding-support-resources-to-your-project
|
|
|
|
Reviewed-by: Zimmi48
|
|
Since their introduction, these notations were incorrectly using the
proof-local environment.
|
|
Using pstate makes no sense for printing global stuff
|
