| Age | Commit message (Collapse) | Author |
|---|
|
|
|
At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.
|
|
Reviewed-by: SkySkimmer
|
|
Addendum to #14039 .
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Tweaks to docs that are independent / unrelated to that PR.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
Paramcoq is typically flaky on our worker configuration, c.f.
https://gitlab.com/coq/coq/-/jobs/1144081161
|
|
< 4.07.0
Reviewed-by: JasonGross
Ack-by: jfehrle
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
This seems the official name, the byterun name is just an artifact
from the very preliminary dune build.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: mattam82
|
|
Reviewed-by: pi8027
|
|
Ack-by: gares
Reviewed-by: ppedrot
|
|
The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.
We fix this by adding dummy parameter arguments on sight.
Fixes #14009: TC search failure with primitive projections.
|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
[structures]
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: MSoegtropIMC
|
|
Fixes #10704
|
|
dependencies: Le, Gt, Minus, Lt, Setoid
Reviewed-by: anton-trunov
|
|
Reviewed-by: ejgallego
|
|
|
|
Dependencies for Caml files was removed in PR #11589, but some
parts of it survived in the man page.
|
|
The documentation of extraction became outdated when the big.ml wrapper
got modified by 094e4649c29e2426daca0476c140439de901dafe.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented.
Fixes #13996: missing Ltac1.to_ident.
|
|
|
|
|
|
|
|
|
|
|
|
PArray.set has arity 4, but due to the polymorphic universe, its actual
arity is 5. As a consequence, Kshort_apply cannot be used to invoke it
(or rather its accumulating version).
Using Kapply does not quite work here, because Kpush_retaddr would have to
be invoked before the arguments, that is, before we even know whether the
arguments are accumulators. So, to use Kapply, one would need to push the
return address, push duplicates of the already computed arguments, call
the accumulator, and then pop the original arguments.
This commit follows a simpler approach, but more restrictive, as it is
still limited to arity 4, but this time independently from universes. To
do so, the call is performed in two steps. First, a closure containing the
universes is created. Second, the actual application to the original
arguments is performed, for which Kshort_apply is sufficient.
So, this is inefficient, because a closure is created just so that it can
be immediately fully applied. But since this is the accumulator slow path,
this does not matter.
|
|
Despite their names, APPLY1 to APPLY4 are completely different from
APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return
address was already pushed on the stack, before the arguments were. On the
other hand, APPLY1 to APPLY4 insert the return address in the middle of
the already pushed arguments.
|
|
|
|
This avoids having to drop the last element of the signature in the
common case.
|
|
Reviewed-by: silene
|
|
Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`. Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.
Fixes #14011
|
|
|
|
|
|
Bytecode execution of persistent arrays can modify structured values meant
to be marshalled in vo files. Some VM values are not marshallable, leading
to this anomaly.
There are further issues with the use of a hash table to store structured
values, since they rely on structural equality and hashing functions.
Persistent arrays are not safe in this context.
Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
|
