| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
We already thread the evar map
|
|
We already thread the evar map
|
|
This function already returns the evar map so no problem.
|
|
It goes in an error message so should be fine.
|
|
add an overlay for coquelicot
remove functions from RList: In, Rlength, cons_Rlist, app_RList
because they are essentially the same as In, length, app, and map from List
(beware that the order of arguments changes for map, and the In function
contains reversed equalities).
adds deprecation warnings for Rlist and Rlength
adds deprecated notations for RList.cons and RList.nil
|
|
|
|
Reviewed-by: ppedrot
|
|
notations (+ a fix about locations)
Reviewed-by: ppedrot
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
data from a part where it should never access it.
|
|
This was the only part in the kernel that really relied on the contents
of the Monomorphic node.
|
|
|
|
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
We thread explicitly the evar map everywhere for this purpose.
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
+ tests in the test-suite for non max local implicit arguments
|
|
|
|
|
|
|
|
|
|
|
|
termination checker.
Reviewed-by: SkySkimmer
|
|
There was an evar leak due to an evarmap not being threaded correctly
when computing open terms.
|
|
Reviewed-by: fajb
|
|
Ack-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
Reviewed-by: ejgallego
|
|
Fixes #5617.
|
|
The only user is merely observing whether this can be an rel / var alias.
|
|
It turns out that eagerly computing the lift of huge terms when it is not
used is not great for performance.
Fixes part of #11488.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
extraction.
Reviewed-by: maximedenes
|
|
Ack-by: aspiwack
Reviewed-by: ppedrot
|
|
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2,
only with the pinned version, and bedrock2 is still relatively unstable.
So we make the CI not have Fiat-Crypto depend on bedrock2, and instead
use the pinned submodule, by using `EXTERNAL_REWRITER=1
EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
|
|
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
|
|
Reviewed-by: ejgallego
|
|
native_compute)
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
references
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
|
|
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
|
|
The computation of which files to build is now mostly cached rather than
computed, eliminting basically all of the wait-time from `make` to the
first invocation of `coqc`.
Note that we no longer need to invoke
`./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds
up `coqdep` somewhat significantly.
Fixes #9298
|
|
Contributors are *not* required to prepare all the patches by
themselves. They can request help from project authors, who should be
ready to take part in this.
Also, finish replacing "development" by the more appropriate word
"project".
|
|
|
|
This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.
The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
|
