| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: RalfJung
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes
|
|
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
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
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
|
|
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.
|
|
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
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
|
|
|
|
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
|
|
|
|
|
|
We list preexisting undefined tokens explicitly in
`doc/sphinx/conf.py` and prevent new ones from being introduced by
making it a fatal warning.
This list should be seen as a TODO. Once it is emptied, #9411 can be
closed.
|
|
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
binding semantics.
Ack-by: Zimmi48
|
|
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
|
|
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
vernac
Reviewed-by: maximedenes
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
