| Age | Commit message (Collapse) | Author |
|---|
|
Not needed since we don't allow anonymous Declare Instance
anymore (was needed for factorization or some such before that I think)
|
|
We never use this id in rewrite.ml so don't bother threading it around.
|
|
|
|
|
|
keeping with doc recommendations
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
proof diffs
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Ack-by: erikmd
|
|
|
|
|
|
This lets us avoid having to cache the SearchBlacklist.elements call
in search as we can just use the set module's for_all function.
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
|
|
|
|
|
|
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
|
|
|
